Theorem exp31 356

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp31.1	⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
exp31	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp31

Step	Hyp	Ref	Expression
1		exp31.1	. . 3 ⊢ (((𝜑 ∧ 𝜓) ∧ 𝜒) → 𝜃)
2	1	ex 113	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 113	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 102

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 106

This theorem is referenced by:  exp41  362  exp42  363  expl  370  exbiri  374  anasss  391  an31s  535  con4biddc  788  3impa  1134  exp516  1159  r19.29af2  2502  mpteqb  5315  dffo3  5368  fconstfvm  5433  fliftfun  5489  tfrlem1  5979  tfrlem9  5990  tfr1onlemaccex  6019  tfrcllemaccex  6032  tfrcl  6035  nnsucsssuc  6158  nnaordex  6189  diffifi  6452  prarloclemup  6824  genpcdl  6848  genpcuu  6849  negf1o  7630  recexap  7887  zaddcllemneg  8548  zdiv  8593  uzaddcl  8832  fz0fzelfz0  9292  fz0fzdiffz0  9295  elfzmlbp  9297  difelfzle  9299  fzo1fzo0n0  9346  ssfzo12bi  9388  exfzdc  9403  modfzo0difsn  9554  frecuzrdgg  9575  iseqvalt  9609  expivallem  9651  expcllem  9661  expap0  9680  mulexp  9689  cjexp  10006  absexp  10191  fimaxre2  10335  divconjdvds  10482  addmodlteqALT  10492  divalglemeunn  10553  divalglemeuneg  10555  zsupcllemstep  10573  bezoutlemstep  10618  bezoutlemmain  10619  dfgcd2  10635  pw2dvdslemn  10775