Theorem exp32 422

Description: An exportation inference. (Contributed by NM, 26-Apr-1994.)

Hypothesis

Ref	Expression
exp32.1	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)

Assertion

Ref	Expression
exp32	⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Proof of Theorem exp32

Step	Hyp	Ref	Expression
1		exp32.1	. . 3 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
2	1	ex 414	. 2 ⊢ (𝜑 → ((𝜓 ∧ 𝜒) → 𝜃))
3	2	expd 417	1 ⊢ (𝜑 → (𝜓 → (𝜒 → 𝜃)))

Syntax hints:   → wi 4   ∧ wa 397

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 398

This theorem is referenced by:  exp44  439  exp45  440  expr  458  anassrs  469  an13s  649  3impb  1115  wereu  5596  f0rn0  6689  funfvima3  7144  isomin  7240  isoini  7241  ovg  7469  elovmpt3rab1  7561  onint  7672  peano5  7772  peano5OLD  7773  tfrlem11  8250  tz7.48lem  8303  oalimcl  8422  oaass  8423  resixpfo  8755  fundmen  8856  ssfiALT  8995  php3  9033  php3OLD  9045  fodomfi  9136  marypha1lem  9236  card2inf  9358  ixpiunwdom  9393  cantnflt  9474  cnfcom  9502  dfac3  9923  dfac5lem5  9929  dfac5  9930  cfcoflem  10074  fin1a2s  10216  zorn2lem4  10301  zorn2lem7  10304  fpwwe2lem11  10443  wunfi  10523  grur1a  10621  addcanpi  10701  mulcanpi  10702  distrlem1pr  10827  ltaddpr  10836  ltexprlem1  10838  ltexprlem6  10843  ltexprlem7  10844  prodgt0  11868  mulgt1  11880  uzwo  12697  xmulasslem  13065  xlemul1a  13068  faclbnd  14050  swrdwrdsymb  14420  pfxccatin12lem2a  14485  pfxccat3  14492  swrdccat  14493  cshwidxmod  14561  s3iunsndisj  14724  dvdsaddre2b  16061  divgcdcoprm0  16415  cncongr2  16418  infpnlem1  16656  isacs4lem  18307  cycsubm  18866  gsmsymgrfixlem1  19080  gsmsymgrfix  19081  dmdprdsplit2lem  19693  pgpfac1  19728  pgpfac  19732  lssssr  20260  islmhm2  20345  lspdisj  20432  cygznlem2a  20820  lindfmm  21079  scmataddcl  21710  scmatsubcl  21711  scmatmulcl  21712  cpmatacl  21910  cayhamlem3  22081  cayleyhamilton1  22086  neindisj  22313  cnpnei  22460  t0dist  22521  ordthauslem  22579  uncmp  22599  fiuncmp  22600  iunconnlem  22623  fbasrn  23080  rnelfmlem  23148  rnelfm  23149  fmfnfmlem2  23151  fmfnfmlem4  23153  fclscf  23221  alexsubALTlem3  23245  alexsubALTlem4  23246  alexsubALT  23247  reconn  24036  fsumcn  24078  ovolfiniun  24710  dyadmax  24807  dyadmbllem  24808  dvmptfsum  25184  dvlip2  25204  dvivthlem1  25217  dvcnvrelem1  25226  ply1divex  25346  fta1g  25377  plydivex  25502  fta1  25513  mulcxp  25885  zabsle1  26489  lgsquad2lem2  26578  2lgsoddprm  26609  pntlem3  26802  brbtwn  27312  brcgr  27313  brbtwn2  27318  axeuclid  27376  finsumvtxdg2size  27962  uhgrwkspthlem2  28167  crctcshwlkn0  28231  wwlksnred  28302  wwlksnextinj  28309  umgr2wlk  28359  elwwlks2  28376  clwlkclwwlklem2a  28407  clwlkclwwlkf1lem3  28415  eupth2lems  28647  numclwwlk2lem1lem  28751  frgrregord013  28804  grpoidinvlem3  28913  shorth  29702  pjhthmo  29709  pjpjpre  29826  elspansn5  29981  lnopmi  30407  adjlnop  30493  leopmul2i  30542  stlesi  30648  ssmd2  30719  dmdsl3  30722  mdexchi  30742  cvexchlem  30775  atcv1  30787  atcvatlem  30792  atabsi  30808  mdsymlem2  30811  mdsymlem5  30814  sumdmdii  30822  sumdmdlem  30825  sumdmdlem2  30826  dya2iocnrect  32293  bnj571  32931  pconnconn  33238  iccllysconn  33257  satffunlem2lem1  33411  poseq  33847  nodenselem8  33939  nocvxmin  34018  cgrextend  34355  btwnexch2  34370  colineardim1  34408  lineext  34423  btwnconn1lem13  34446  btwnconn1lem14  34447  seglecgr12im  34457  outsideofeq  34477  outsideofeu  34478  nn0prpwlem  34556  neibastop2lem  34594  tailfb  34611  nndivsub  34691  ee7.2aOLD  34695  fvineqsneu  35626  poimirlem31  35852  heicant  35856  filbcmb  35942  prdsbnd2  35997  heibor  36023  rngoisocnv  36183  ax12eq  36997  ax12el  36998  pmodlem2  37903  cdleme22b  38397  cdleme32d  38500  cdleme32f  38502  trlord  38625  cdlemj2  38878  cdlemk38  38971  cdlemk19x  38999  dihord2pre  39281  fsuppind  40316  mzpcompact2lem  40610  pellfundex  40745  acongsym  40836  pwssplit4  40952  pwslnm  40957  relexpmulg  41356  stoweidlem17  43607  2reu8i  44663  imasetpreimafvbijlemf1  44914  iccpartigtl  44933  paireqne  45021  fmtnofac2lem  45078  2pwp1prmfmtno  45100  lighneallem4  45120  bgoldbtbndlem2  45316  bgoldbtbndlem3  45317  bgoldbtbnd  45319  lmod0rng  45484  2zrngamgm  45555