Theorem exp31 364

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 115	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 115	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  exp41  370  exp42  371  expl  378  exbiri  382  anasss  399  an31s  570  con4biddc  858  3impa  1196  exp516  1229  rexlimdva2  2614  r19.29af2  2634  disjiun  4024  mpteqb  5648  dffo3  5705  fconstfvm  5776  fliftfun  5839  tfrlem1  6361  tfrlem9  6372  tfr1onlemaccex  6401  tfrcllemaccex  6414  tfrcl  6417  nnsucsssuc  6545  nnaordex  6581  diffifi  6950  fidcenumlemrk  7013  fidcenumlemr  7014  nninfninc  7182  nnnninfeq  7187  nnnninfeq2  7188  exmidontriimlem4  7284  exmidontriim  7285  prarloclemup  7555  genpcdl  7579  genpcuu  7580  negf1o  8401  recexap  8672  zaddcllemneg  9356  zdiv  9405  uzaddcl  9651  fz0fzelfz0  10193  fz0fzdiffz0  10196  elfzmlbp  10198  difelfzle  10200  fzo1fzo0n0  10250  ssfzo12bi  10292  exfzdc  10307  modfzo0difsn  10466  frecuzrdgg  10487  seq3val  10531  seqvalcd  10532  seqf1og  10592  exp3vallem  10611  expcllem  10621  expap0  10640  mulexp  10649  cjexp  11037  absexp  11223  fimaxre2  11370  summodc  11526  fsum2d  11578  modfsummod  11601  binom  11627  clim2prod  11682  fprod2d  11766  efexp  11825  demoivreALT  11917  divconjdvds  11991  addmodlteqALT  12001  divalglemeunn  12062  divalglemeuneg  12064  zsupcllemstep  12082  bezoutlemstep  12134  bezoutlemmain  12135  dfgcd2  12151  pw2dvdslemn  12303  oddprmdvds  12492  sgrpidmndm  13001  gsumfzz  13067  srgmulgass  13485  ringinvnzdiv  13546  lmodvsmmulgdi  13819  topbas  14235  cnplimclemr  14823  limccnp2lem  14830  gausslemma2dlem3  15179  nninfalllem1  15498  nninfsellemdc  15500  nninfsellemqall  15505  isomninnlem  15520  trirec0  15534  ismkvnnlem  15542