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  534  con4biddc  787  3impa  1133  exp516  1158  r19.29af2  2496  mpteqb  5282  dffo3  5335  fconstfvm  5400  fliftfun  5456  tfrlem1  5946  tfrlem9  5958  nnsucsssuc  6094  nnaordex  6123  diffifi  6378  prarloclemup  6685  genpcdl  6709  genpcuu  6710  negf1o  7486  recexap  7743  zaddcllemneg  8390  zdiv  8435  uzaddcl  8674  fz0fzelfz0  9138  fz0fzdiffz0  9141  elfzmlbp  9143  difelfzle  9145  fzo1fzo0n0  9192  ssfzo12bi  9234  exfzdc  9249  modfzo0difsn  9397  expivallem  9477  expcllem  9487  expap0  9506  mulexp  9515  cjexp  9780  absexp  9965  fimaxre2  10109  divconjdvds  10249  addmodlteqALT  10259  divalglemeunn  10321  divalglemeuneg  10323  zsupcllemstep  10341  bezoutlemstep  10386  bezoutlemmain  10387  dfgcd2  10403  pw2dvdslemn  10543