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  2665  r19.29af2  2685  disjiun  4109  mpteqb  5773  dffo3  5829  fconstfvm  5907  fliftfun  5975  elabreximd  6329  tfrlem1  6552  tfrlem9  6563  tfr1onlemaccex  6592  tfrcllemaccex  6605  tfrcl  6608  nnsucsssuc  6738  nnaordex  6774  diffifi  7164  fidcenumlemrk  7237  fidcenumlemr  7238  nninfninc  7427  nnnninfeq  7432  nnnninfeq2  7433  exmidontriimlem4  7544  exmidontriim  7545  prarloclemup  7826  genpcdl  7850  genpcuu  7851  negf1o  8673  recexap  8945  zaddcllemneg  9636  zdiv  9687  uzaddcl  9939  fz0fzelfz0  10486  fz0fzdiffz0  10489  elfzmlbp  10491  difelfzle  10493  fzo1fzo0n0  10547  elincfzoext  10563  ssfzo12bi  10595  exfzdc  10611  zsupcllemstep  10614  modfzo0difsn  10784  frecuzrdgg  10805  seq3val  10849  seqvalcd  10850  seqf1og  10910  exp3vallem  10929  expcllem  10939  expap0  10958  mulexp  10967  swrdnd  11379  swrdswrdlem  11424  swrdswrd  11425  pfxccat3  11454  reuccatpfxs1  11467  cjexp  11606  absexp  11793  fimaxre2  11941  summodc  12098  fsum2d  12150  modfsummod  12173  binom  12199  clim2prod  12254  fprod2d  12338  efexp  12397  demoivreALT  12489  divconjdvds  12564  addmodlteqALT  12574  divalglemeunn  12636  divalglemeuneg  12638  bezoutlemstep  12722  bezoutlemmain  12723  dfgcd2  12739  pw2dvdslemn  12891  oddprmdvds  13081  sgrpidmndm  13685  gsumfzz  13754  srgmulgass  14236  ringinvnzdiv  14297  lmodvsmmulgdi  14601  topbas  15062  cnplimclemr  15664  limccnp2lem  15671  gausslemma2dlem3  16066  upgriswlkdc  16485  clwwlkccatlem  16525  umgr2cwwk2dif  16549  clwwlknonex2  16564  depindlem2  16632  depindlem3  16633  nninfalllem1  16926  nninfsellemdc  16928  nninfsellemqall  16933  isomninnlem  16954  trirec0  16968  ismkvnnlem  16977