Theorem exp31 293

Description: An exportation inference.

Hypothesis

Ref	Expression
exp31.1	⊢ (((φ ∧ ψ) ∧ χ) → θ)

Assertion

Ref	Expression
exp31	⊢ (φ → (ψ → (χ → θ)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 ⊢ (((φ ∧ ψ) ∧ χ) → θ)
2	1	exp 291	. 2 ⊢ ((φ ∧ ψ) → (χ → θ))
3	2	exp 291	1 ⊢ (φ → (ψ → (χ → θ)))

Syntax hints:   → wi 2   ∧ wa 196

This theorem is referenced by:  exp41 299  exp42 300  adantlll 313  adantlrl 314  adantlrr 315  anasss 337  3impa 609  3exp 611  pwssun 1917  onmindif 2312  ordsucss 2320  ordsucelsuc 2324  tfindsg 2402  tfindsg2 2403  fvco2 2866  fconstfv 2903  tfrlem9 2957  tz7.49c 2998  oaordi 3148  oaordex 3160  oaass 3163  oen0 3165  nnaordex 3191  nnawordex 3192  omsmolem 3195  sdomen2 3380  mapenlem1 3384  mapenlem2 3385  ssenen 3399  php3 3411  finsucdom 3421  pssnn 3428  fiint 3445  tz9.12lem3 3505  rankr1 3518  zornlem6 3608  fodom 3613  unxpdomlem 3649  ondomon 3662  axrepnd 3740  ltrpq 3879  genpcd 3903  1idpr 3927  prlem934a 3931  ltexprlem6 3941  ltexprlem7 3942  mulgt0sr 4008  recexsr 4010  ssgt0sr 4011  suppsr2 4017  suppsr3 4018  axnegex 4078  nnleltp1t 4448  nndiv 4453  zltp1let 4597  zneo 4601  uzwo 4605  uzwo2 4606  nnwoOLD 4608  zmax 4618  zbtwnre 4619  qret 4631  expcllem 4682  sqr2irrlem3 4779  infmap2 4953  shmods 5363  spansncol 5473  h1datom 5483  osumlem4 5533  osumlem6 5535  pjss2co 5634  pj3cor1 5661  atcvat4 5775  mds mlem3 5778  mdsymlem4 5779  sumdmdi 5785

This theorem was proved from axioms:  ax-1 3  ax-2 4  ax-3 5  ax-mp 6

This theorem depends on definitions:  df-bi 128  df-an 198

metamath.org