Theorem exp31 359

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 114	. 2 ⊢ ((𝜑 ∧ 𝜓) → (𝜒 → 𝜃))
3	2	ex 114	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 103

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia3 107

This theorem is referenced by:  exp41  365  exp42  366  expl  373  exbiri  377  anasss  394  an31s  542  con4biddc  825  3impa  1159  exp516  1188  rexlimdva2  2526  r19.29af2  2546  disjiun  3890  mpteqb  5465  dffo3  5521  fconstfvm  5592  fliftfun  5651  tfrlem1  6159  tfrlem9  6170  tfr1onlemaccex  6199  tfrcllemaccex  6212  tfrcl  6215  nnsucsssuc  6342  nnaordex  6377  diffifi  6741  fidcenumlemrk  6794  fidcenumlemr  6795  prarloclemup  7251  genpcdl  7275  genpcuu  7276  negf1o  8063  recexap  8327  zaddcllemneg  8997  zdiv  9043  uzaddcl  9283  fz0fzelfz0  9797  fz0fzdiffz0  9800  elfzmlbp  9802  difelfzle  9804  fzo1fzo0n0  9853  ssfzo12bi  9895  exfzdc  9910  modfzo0difsn  10061  frecuzrdgg  10082  seq3val  10124  seqvalcd  10125  exp3vallem  10187  expcllem  10197  expap0  10216  mulexp  10225  cjexp  10558  absexp  10743  fimaxre2  10890  summodc  11044  fsum2d  11096  modfsummod  11119  binom  11145  efexp  11239  demoivreALT  11330  divconjdvds  11395  addmodlteqALT  11405  divalglemeunn  11466  divalglemeuneg  11468  zsupcllemstep  11486  bezoutlemstep  11531  bezoutlemmain  11532  dfgcd2  11548  pw2dvdslemn  11688  topbas  12079  cnplimclemr  12594  limccnp2lem  12601  nninfalllemn  12894  nninfalllem1  12895  nninfsellemdc  12898  nninfsellemqall  12903  isomninnlem  12917