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  403  an31s  576  con4biddc  869  3impa  1225  exp516  1258  rexlimdva2  2671  r19.29af2  2691  disjiun  4123  mpteqb  5793  dffo3  5849  fconstfvm  5927  fliftfun  5996  elabreximd  6350  tfrlem1  6573  tfrlem9  6584  tfr1onlemaccex  6613  tfrcllemaccex  6626  tfrcl  6629  nnsucsssuc  6759  nnaordex  6795  diffifi  7192  fidcenumlemrk  7265  fidcenumlemr  7266  nninfninc  7457  nnnninfeq  7462  nnnninfeq2  7463  exmidontriimlem4  7574  exmidontriim  7575  prarloclemup  7856  genpcdl  7880  genpcuu  7881  negf1o  8703  recexap  8975  zaddcllemneg  9666  zdiv  9717  uzaddcl  9969  fz0fzelfz0  10517  fz0fzdiffz0  10520  elfzmlbp  10522  difelfzle  10524  fzo1fzo0n0  10578  elincfzoext  10594  ssfzo12bi  10626  exfzdc  10642  zsupcllemstep  10645  modfzo0difsn  10815  frecuzrdgg  10836  seq3val  10880  seqvalcd  10881  seqf1og  10941  exp3vallem  10960  expcllem  10970  expap0  10989  mulexp  10998  swrdnd  11414  swrdswrdlem  11459  swrdswrd  11460  pfxccat3  11489  reuccatpfxs1  11502  cjexp  11641  absexp  11828  fimaxre2  11976  summodc  12133  fsum2d  12185  modfsummod  12208  binom  12234  clim2prod  12289  fprod2d  12373  efexp  12432  demoivreALT  12524  divconjdvds  12599  addmodlteqALT  12609  divalglemeunn  12671  divalglemeuneg  12673  bezoutlemstep  12757  bezoutlemmain  12758  dfgcd2  12774  pw2dvdslemn  12926  oddprmdvds  13116  sgrpidmndm  13716  srgmulgass  14276  ringinvnzdiv  14338  lmodvsmmulgdi  14643  assamulgscmlem2  15025  topbas  15151  cnplimclemr  15753  limccnp2lem  15760  gausslemma2dlem3  16165  upgriswlkdc  16584  clwwlkccatlem  16624  umgr2cwwk2dif  16648  clwwlknonex2  16663  depindlem2  16731  depindlem3  16732  nninfalllem1  17025  nninfsellemdc  17027  nninfsellemqall  17032  isomninnlem  17053  trirec0  17067  ismkvnnlem  17076