Theorem exp32 420

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

Syntax hints:   → wi 4   ∧ wa 395

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 207  df-an 396

This theorem is referenced by:  exp44  437  exp45  438  expr  456  anassrs  467  an13s  652  3impb  1115  wereu  5628  f0rn0  6727  funfvima3  7192  dff14i  7215  isomin  7293  isoini  7294  ovg  7533  elovmpt3rab1  7628  onint  7745  peano5  7845  poseq  8110  tfrlem11  8329  tz7.48lem  8382  oalimcl  8497  oaass  8498  resixpfo  8886  fundmen  8980  ssfiALT  9110  php3  9145  fodomfi  9224  fodomfiOLD  9242  marypha1lem  9348  card2inf  9472  ixpiunwdom  9507  cantnflt  9593  cnfcom  9621  dfac3  10043  dfac5lem5  10049  dfac5  10051  cfcoflem  10194  fin1a2s  10336  zorn2lem4  10421  zorn2lem7  10424  fpwwe2lem11  10564  wunfi  10644  grur1a  10742  addcanpi  10822  mulcanpi  10823  distrlem1pr  10948  ltaddpr  10957  ltexprlem1  10959  ltexprlem6  10964  ltexprlem7  10965  prodgt0  12000  mulgt1OLD  12012  uzwo  12836  xmulasslem  13212  xlemul1a  13215  faclbnd  14225  swrdwrdsymb  14598  pfxccatin12lem2a  14662  pfxccat3  14669  swrdccat  14670  cshwidxmod  14738  s3iunsndisj  14903  dvdsaddre2b  16246  divgcdcoprm0  16604  cncongr2  16607  infpnlem1  16850  isacs4lem  18479  cycsubm  19143  gsmsymgrfixlem1  19368  gsmsymgrfix  19369  imasabl  19817  dmdprdsplit2lem  19988  pgpfac1  20023  pgpfac  20027  lssssr  20917  islmhm2  21002  lspdisj  21092  pzriprnglem5  21452  pzriprnglem8  21455  cygznlem2a  21534  lindfmm  21794  scmataddcl  22472  scmatsubcl  22473  scmatmulcl  22474  cpmatacl  22672  cayhamlem3  22843  cayleyhamilton1  22848  neindisj  23073  cnpnei  23220  t0dist  23281  ordthauslem  23339  uncmp  23359  fiuncmp  23360  iunconnlem  23383  fbasrn  23840  rnelfmlem  23908  rnelfm  23909  fmfnfmlem2  23911  fmfnfmlem4  23913  fclscf  23981  alexsubALTlem3  24005  alexsubALTlem4  24006  alexsubALT  24007  reconn  24785  fsumcn  24829  ovolfiniun  25470  dyadmax  25567  dyadmbllem  25568  dvmptfsum  25947  dvlip2  25968  dvivthlem1  25981  dvcnvrelem1  25990  ply1divex  26110  fta1g  26143  plydivex  26273  fta1  26284  mulcxp  26662  zabsle1  27275  lgsquad2lem2  27364  2lgsoddprm  27395  pntlem3  27588  nodenselem8  27671  nocvxmin  27763  precsexlem11  28225  om2noseqrdg  28312  expadds  28443  brbtwn  28984  brcgr  28985  brbtwn2  28990  axeuclid  29048  finsumvtxdg2size  29636  uhgrwkspthlem2  29839  crctcshwlkn0  29906  wwlksnred  29977  wwlksnextinj  29984  umgr2wlk  30034  elwwlks2  30054  clwlkclwwlklem2a  30085  clwlkclwwlkf1lem3  30093  eupth2lems  30325  numclwwlk2lem1lem  30429  frgrregord013  30482  grpoidinvlem3  30593  shorth  31382  pjhthmo  31389  pjpjpre  31506  elspansn5  31661  lnopmi  32087  adjlnop  32173  leopmul2i  32222  stlesi  32328  ssmd2  32399  dmdsl3  32402  mdexchi  32422  cvexchlem  32455  atcv1  32467  atcvatlem  32472  atabsi  32488  mdsymlem2  32491  mdsymlem5  32494  sumdmdii  32502  sumdmdlem  32505  sumdmdlem2  32506  dya2iocnrect  34458  bnj571  35081  pconnconn  35444  iccllysconn  35463  satffunlem2lem1  35617  cgrextend  36221  btwnexch2  36236  colineardim1  36274  lineext  36289  btwnconn1lem13  36312  btwnconn1lem14  36313  seglecgr12im  36323  outsideofeq  36343  outsideofeu  36344  nn0prpwlem  36535  neibastop2lem  36573  tailfb  36590  nndivsub  36670  ee7.2aOLD  36674  fvineqsneu  37660  poimirlem31  37896  heicant  37900  filbcmb  37985  prdsbnd2  38040  heibor  38066  rngoisocnv  38226  ax12eq  39311  ax12el  39312  pmodlem2  40217  cdleme22b  40711  cdleme32d  40814  cdleme32f  40816  trlord  40939  cdlemj2  41192  cdlemk38  41285  cdlemk19x  41313  dihord2pre  41595  fsuppind  42942  mzpcompact2lem  43102  pellfundex  43237  acongsym  43327  pwssplit4  43440  pwslnm  43445  cantnfresb  43675  relexpmulg  44060  relpmin  45302  stoweidlem17  46369  2reu8i  47467  imasetpreimafvbijlemf1  47758  iccpartigtl  47777  paireqne  47865  fmtnofac2lem  47922  2pwp1prmfmtno  47944  lighneallem4  47964  bgoldbtbndlem2  48160  bgoldbtbndlem3  48161  bgoldbtbnd  48163  grimco  48243  isuspgrimlem  48249  cycl3grtri  48301  isubgr3stgrlem6  48325  lmod0rng  48583  2zrngamgm  48599