Theorem exp32 424

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

Syntax hints:   → wi 4   ∧ wa 399

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 210  df-an 400

This theorem is referenced by:  exp44  441  exp45  442  expr  460  anassrs  471  an13s  651  3impb  1116  wereu  5522  f0rn0  6564  funfvima3  7012  isomin  7106  isoini  7107  ovg  7332  elovmpt3rab1  7424  onint  7532  peano5  7627  peano5OLD  7628  tfrlem11  8056  tz7.48lem  8109  oalimcl  8220  oaass  8221  resixpfo  8549  fundmen  8633  php3  8756  ssfiOLD  8819  fodomfi  8873  marypha1lem  8973  card2inf  9095  ixpiunwdom  9130  cantnflt  9211  cnfcom  9239  dfac3  9624  dfac5lem5  9630  dfac5  9631  cfcoflem  9775  fin1a2s  9917  zorn2lem4  10002  zorn2lem7  10005  fpwwe2lem11  10144  wunfi  10224  grur1a  10322  addcanpi  10402  mulcanpi  10403  distrlem1pr  10528  ltaddpr  10537  ltexprlem1  10539  ltexprlem6  10544  ltexprlem7  10545  prodgt0  11568  mulgt1  11580  uzwo  12396  xmulasslem  12764  xlemul1a  12767  faclbnd  13745  swrdwrdsymb  14116  pfxccatin12lem2a  14181  pfxccat3  14188  swrdccat  14189  cshwidxmod  14257  s3iunsndisj  14420  dvdsaddre2b  15755  divgcdcoprm0  16109  cncongr2  16112  infpnlem1  16349  isacs4lem  17897  cycsubm  18466  gsmsymgrfixlem1  18676  gsmsymgrfix  18677  dmdprdsplit2lem  19289  pgpfac1  19324  pgpfac  19328  lssssr  19847  islmhm2  19932  lspdisj  20019  cygznlem2a  20389  lindfmm  20646  scmataddcl  21270  scmatsubcl  21271  scmatmulcl  21272  cpmatacl  21470  cayhamlem3  21641  cayleyhamilton1  21646  neindisj  21871  cnpnei  22018  t0dist  22079  ordthauslem  22137  uncmp  22157  fiuncmp  22158  iunconnlem  22181  fbasrn  22638  rnelfmlem  22706  rnelfm  22707  fmfnfmlem2  22709  fmfnfmlem4  22711  fclscf  22779  alexsubALTlem3  22803  alexsubALTlem4  22804  alexsubALT  22805  reconn  23583  fsumcn  23625  ovolfiniun  24256  dyadmax  24353  dyadmbllem  24354  dvmptfsum  24730  dvlip2  24750  dvivthlem1  24763  dvcnvrelem1  24772  ply1divex  24892  fta1g  24923  plydivex  25048  fta1  25059  mulcxp  25431  zabsle1  26035  lgsquad2lem2  26124  2lgsoddprm  26155  pntlem3  26348  brbtwn  26848  brcgr  26849  brbtwn2  26854  axeuclid  26912  finsumvtxdg2size  27495  uhgrwkspthlem2  27698  crctcshwlkn0  27762  wwlksnred  27833  wwlksnextinj  27840  umgr2wlk  27890  elwwlks2  27907  clwlkclwwlklem2a  27938  clwlkclwwlkf1lem3  27946  eupth2lems  28178  numclwwlk2lem1lem  28282  frgrregord013  28335  grpoidinvlem3  28444  shorth  29233  pjhthmo  29240  pjpjpre  29357  elspansn5  29512  lnopmi  29938  adjlnop  30024  leopmul2i  30073  stlesi  30179  ssmd2  30250  dmdsl3  30253  mdexchi  30273  cvexchlem  30306  atcv1  30318  atcvatlem  30323  atabsi  30339  mdsymlem2  30342  mdsymlem5  30345  sumdmdii  30353  sumdmdlem  30356  sumdmdlem2  30357  dya2iocnrect  31821  bnj571  32460  pconnconn  32767  iccllysconn  32786  satffunlem2lem1  32940  trpredmintr  33378  poseq  33418  nodenselem8  33540  nocvxmin  33619  cgrextend  33956  btwnexch2  33971  colineardim1  34009  lineext  34024  btwnconn1lem13  34047  btwnconn1lem14  34048  seglecgr12im  34058  outsideofeq  34078  outsideofeu  34079  nn0prpwlem  34157  neibastop2lem  34195  tailfb  34212  nndivsub  34292  ee7.2aOLD  34296  fvineqsneu  35228  poimirlem31  35454  heicant  35458  filbcmb  35544  prdsbnd2  35599  heibor  35625  rngoisocnv  35785  ax12eq  36601  ax12el  36602  pmodlem2  37507  cdleme22b  38001  cdleme32d  38104  cdleme32f  38106  trlord  38229  cdlemj2  38482  cdlemk38  38575  cdlemk19x  38603  dihord2pre  38885  fsuppind  39881  mzpcompact2lem  40168  pellfundex  40303  acongsym  40393  pwssplit4  40509  pwslnm  40514  relexpmulg  40887  stoweidlem17  43123  2reu8i  44168  imasetpreimafvbijlemf1  44420  iccpartigtl  44439  paireqne  44527  fmtnofac2lem  44584  2pwp1prmfmtno  44606  lighneallem4  44626  bgoldbtbndlem2  44822  bgoldbtbndlem3  44823  bgoldbtbnd  44825  lmod0rng  44990  2zrngamgm  45061