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  857  3impa  1194  exp516  1227  rexlimdva2  2597  r19.29af2  2617  disjiun  3996  mpteqb  5603  dffo3  5660  fconstfvm  5731  fliftfun  5792  tfrlem1  6304  tfrlem9  6315  tfr1onlemaccex  6344  tfrcllemaccex  6357  tfrcl  6360  nnsucsssuc  6488  nnaordex  6524  diffifi  6889  fidcenumlemrk  6948  fidcenumlemr  6949  nnnninfeq  7121  nnnninfeq2  7122  exmidontriimlem4  7218  exmidontriim  7219  prarloclemup  7489  genpcdl  7513  genpcuu  7514  negf1o  8333  recexap  8604  zaddcllemneg  9286  zdiv  9335  uzaddcl  9580  fz0fzelfz0  10120  fz0fzdiffz0  10123  elfzmlbp  10125  difelfzle  10127  fzo1fzo0n0  10176  ssfzo12bi  10218  exfzdc  10233  modfzo0difsn  10388  frecuzrdgg  10409  seq3val  10451  seqvalcd  10452  exp3vallem  10514  expcllem  10524  expap0  10543  mulexp  10552  cjexp  10893  absexp  11079  fimaxre2  11226  summodc  11382  fsum2d  11434  modfsummod  11457  binom  11483  clim2prod  11538  fprod2d  11622  efexp  11681  demoivreALT  11772  divconjdvds  11845  addmodlteqALT  11855  divalglemeunn  11916  divalglemeuneg  11918  zsupcllemstep  11936  bezoutlemstep  11988  bezoutlemmain  11989  dfgcd2  12005  pw2dvdslemn  12155  oddprmdvds  12342  sgrpidmndm  12751  srgmulgass  13072  ringinvnzdiv  13127  topbas  13349  cnplimclemr  13920  limccnp2lem  13927  nninfalllem1  14528  nninfsellemdc  14530  nninfsellemqall  14535  isomninnlem  14549  trirec0  14563  ismkvnnlem  14571