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  572  con4biddc  865  3impa  1221  exp516  1254  rexlimdva2  2663  r19.29af2  2683  disjiun  4103  mpteqb  5767  dffo3  5823  fconstfvm  5901  fliftfun  5968  tfrlem1  6538  tfrlem9  6549  tfr1onlemaccex  6578  tfrcllemaccex  6591  tfrcl  6594  nnsucsssuc  6724  nnaordex  6760  diffifi  7150  fidcenumlemrk  7223  fidcenumlemr  7224  nninfninc  7413  nnnninfeq  7418  nnnninfeq2  7419  exmidontriimlem4  7530  exmidontriim  7531  prarloclemup  7809  genpcdl  7833  genpcuu  7834  negf1o  8654  recexap  8926  zaddcllemneg  9615  zdiv  9665  uzaddcl  9917  fz0fzelfz0  10460  fz0fzdiffz0  10463  elfzmlbp  10465  difelfzle  10467  fzo1fzo0n0  10521  elincfzoext  10537  ssfzo12bi  10569  exfzdc  10585  zsupcllemstep  10588  modfzo0difsn  10756  frecuzrdgg  10777  seq3val  10821  seqvalcd  10822  seqf1og  10882  exp3vallem  10901  expcllem  10911  expap0  10930  mulexp  10939  swrdnd  11347  swrdswrdlem  11392  swrdswrd  11393  pfxccat3  11422  reuccatpfxs1  11435  cjexp  11574  absexp  11760  fimaxre2  11908  summodc  12065  fsum2d  12117  modfsummod  12140  binom  12166  clim2prod  12221  fprod2d  12305  efexp  12364  demoivreALT  12456  divconjdvds  12531  addmodlteqALT  12541  divalglemeunn  12603  divalglemeuneg  12605  bezoutlemstep  12689  bezoutlemmain  12690  dfgcd2  12706  pw2dvdslemn  12858  oddprmdvds  13048  sgrpidmndm  13625  gsumfzz  13700  srgmulgass  14125  ringinvnzdiv  14186  lmodvsmmulgdi  14463  topbas  14924  cnplimclemr  15526  limccnp2lem  15533  gausslemma2dlem3  15928  upgriswlkdc  16347  clwwlkccatlem  16387  umgr2cwwk2dif  16411  clwwlknonex2  16426  depindlem2  16494  depindlem3  16495  nninfalllem1  16778  nninfsellemdc  16780  nninfsellemqall  16785  isomninnlem  16806  trirec0  16820  ismkvnnlem  16829