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 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

This proof depends on syntax axioms:   → wi 4   ∧ wa 104

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia3 108

This theorem is used 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  4125  mpteqb  5796  dffo3  5855  fconstfvm  5933  fliftfun  6002  elabreximd  6356  tfrlem1  6579  tfrlem9  6590  tfr1onlemaccex  6619  tfrcllemaccex  6632  tfrcl  6635  nnsucsssuc  6765  nnaordex  6801  diffifi  7198  fidcenumlemrk  7271  fidcenumlemr  7272  nninfninc  7464  nnnninfeq  7469  nnnninfeq2  7470  exmidontriimlem4  7581  exmidontriim  7582  prarloclemup  7863  genpcdl  7887  genpcuu  7888  negf1o  8711  recexap  8984  zaddcllemneg  9688  zdiv  9739  uzaddcl  9996  fz0fzelfz0  10545  fz0fzdiffz0  10548  elfzmlbp  10550  difelfzle  10552  fzo1fzo0n0  10606  elincfzoext  10622  ssfzo12bi  10654  exfzdc  10670  zsupcllemstep  10673  modfzo0difsn  10846  frecuzrdgg  10867  seq3val  10911  seqvalcd  10912  seqf1og  10972  exp3vallem  10991  expcllem  11001  expap0  11020  mulexp  11029  swrdnd  11446  swrdswrdlem  11491  swrdswrd  11492  pfxccat3  11521  reuccatpfxs1  11534  cjexp  11673  absexp  11861  fimaxre2  12009  summodc  12168  fsum2d  12220  modfsummod  12243  binom  12269  clim2prod  12324  fprod2d  12408  efexp  12467  demoivreALT  12559  divconjdvds  12634  addmodlteqALT  12644  divalglemeunn  12706  divalglemeuneg  12708  bezoutlemstep  12792  bezoutlemmain  12793  dfgcd2  12809  pwbdvdslemn  12962  oddprmdvds  13155  sgrpidmndm  13784  srgmulgass  14344  ringinvnzdiv  14406  lmodvsmmulgdi  14711  assamulgscmlem2  15093  topbas  15220  cnplimclemr  15822  limccnp2lem  15829  gausslemma2dlem3  16304  upgriswlkdc  16723  clwwlkccatlem  16763  umgr2cwwk2dif  16787  clwwlknonex2  16802  depindlem2  16870  depindlem3  16871  nninfalllem1  17173  nninfsellemdc  17175  nninfsellemqall  17180  isomninnlem  17201  trirec0  17215  ismkvnnlem  17224