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  2654  r19.29af2  2674  disjiun  4088  mpteqb  5746  dffo3  5802  fconstfvm  5880  fliftfun  5947  tfrlem1  6517  tfrlem9  6528  tfr1onlemaccex  6557  tfrcllemaccex  6570  tfrcl  6573  nnsucsssuc  6703  nnaordex  6739  diffifi  7126  fidcenumlemrk  7196  fidcenumlemr  7197  nninfninc  7365  nnnninfeq  7370  nnnninfeq2  7371  exmidontriimlem4  7482  exmidontriim  7483  prarloclemup  7758  genpcdl  7782  genpcuu  7783  negf1o  8604  recexap  8876  zaddcllemneg  9561  zdiv  9611  uzaddcl  9863  fz0fzelfz0  10405  fz0fzdiffz0  10408  elfzmlbp  10410  difelfzle  10412  fzo1fzo0n0  10466  elincfzoext  10482  ssfzo12bi  10514  exfzdc  10530  zsupcllemstep  10533  modfzo0difsn  10701  frecuzrdgg  10722  seq3val  10766  seqvalcd  10767  seqf1og  10827  exp3vallem  10846  expcllem  10856  expap0  10875  mulexp  10884  swrdnd  11287  swrdswrdlem  11332  swrdswrd  11333  pfxccat3  11362  reuccatpfxs1  11375  cjexp  11514  absexp  11700  fimaxre2  11848  summodc  12005  fsum2d  12057  modfsummod  12080  binom  12106  clim2prod  12161  fprod2d  12245  efexp  12304  demoivreALT  12396  divconjdvds  12471  addmodlteqALT  12481  divalglemeunn  12543  divalglemeuneg  12545  bezoutlemstep  12629  bezoutlemmain  12630  dfgcd2  12646  pw2dvdslemn  12798  oddprmdvds  12988  sgrpidmndm  13564  gsumfzz  13639  srgmulgass  14064  ringinvnzdiv  14125  lmodvsmmulgdi  14399  topbas  14858  cnplimclemr  15460  limccnp2lem  15467  gausslemma2dlem3  15862  upgriswlkdc  16281  clwwlkccatlem  16321  umgr2cwwk2dif  16345  clwwlknonex2  16360  depindlem2  16428  depindlem3  16429  nninfalllem1  16714  nninfsellemdc  16716  nninfsellemqall  16721  isomninnlem  16742  trirec0  16756  ismkvnnlem  16765