Theorem exp32 629

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

Syntax hints:   → wi 4   ∧ wa 383

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 196  df-an 385

This theorem is referenced by:  exp44  639  exp45  640  expr  641  anassrs  678  an13s  841  3impb  1252  reusv2lem2OLD  4796  wereu  5034  f0rn0  6003  funfvima3  6399  isomin  6487  isoini  6488  ovg  6697  elovmpt3rab1  6791  onint  6887  peano5  6981  tfrlem11  7371  tz7.48lem  7423  oalimcl  7527  oaass  7528  resixpfo  7832  fundmen  7916  php3  8031  ssfi  8065  fodomfi  8124  marypha1lem  8222  card2inf  8343  ixpiunwdom  8379  cantnflt  8452  cnfcom  8480  dfac3  8827  dfac5lem5  8833  dfac5  8834  cfcoflem  8977  fin1a2s  9119  zorn2lem4  9204  zorn2lem7  9207  fpwwe2lem12  9342  wunfi  9422  grur1a  9520  addcanpi  9600  mulcanpi  9601  distrlem1pr  9726  ltaddpr  9735  ltexprlem1  9737  ltexprlem6  9742  ltexprlem7  9743  prodgt0  10747  mulgt1  10761  uzwo  11627  xmulasslem  11987  xlemul1a  11990  faclbnd  12939  swrdccatin12lem2a  13336  swrdccat3  13343  swrdccat  13344  cshwidxmod  13400  s3iunsndisj  13555  dvdsaddre2b  14867  divgcdcoprm0  15217  cncongr2  15220  infpnlem1  15452  isacs4lem  16991  gsmsymgrfixlem1  17670  gsmsymgrfix  17671  dmdprdsplit2lem  18267  pgpfac1  18302  pgpfac  18306  lssssr  18774  islmhm2  18859  lspdisj  18946  cygznlem2a  19735  lindfmm  19985  scmataddcl  20141  scmatsubcl  20142  scmatmulcl  20143  cayhamlem3  20511  cayleyhamilton1  20516  neindisj  20731  cnpnei  20878  t0dist  20939  ordthauslem  20997  uncmp  21016  fiuncmp  21017  iunconlem  21040  fbasrn  21498  rnelfmlem  21566  rnelfm  21567  fmfnfmlem2  21569  fmfnfmlem4  21571  fclscf  21639  alexsubALTlem3  21663  alexsubALTlem4  21664  alexsubALT  21665  reconn  22439  fsumcn  22481  ovolfiniun  23076  dyadmax  23172  dyadmbllem  23173  dvmptfsum  23542  dvlip2  23562  dvivthlem1  23575  dvcnvrelem1  23584  ply1divex  23700  fta1g  23731  plydivex  23856  fta1  23867  mulcxp  24231  zabsle1  24821  lgsquad2lem2  24910  2lgsoddprm  24941  pntlem3  25098  brbtwn  25579  brcgr  25580  brbtwn2  25585  axeuclid  25643  wwlknred  26251  wwlkextinj  26258  clwlkisclwwlklem2a  26313  wwlkext2clwwlk  26331  eupath2  26507  clwwlkextfrlem1  26603  frgraregord013  26645  grpoidinvlem3  26744  shorth  27538  pjhthmo  27545  pjpjpre  27662  elspansn5  27817  lnopmi  28243  adjlnop  28329  leopmul2i  28378  stlesi  28484  ssmd2  28555  dmdsl3  28558  mdexchi  28578  cvexchlem  28611  atcv1  28623  atcvatlem  28628  atabsi  28644  mdsymlem2  28647  mdsymlem5  28650  sumdmdii  28658  sumdmdlem  28661  sumdmdlem2  28662  dya2iocnrect  29670  bnj571  30230  pconcon  30467  iccllyscon  30486  trpredmintr  30975  poseq  30994  nodenselem8  31087  nocvxmin  31090  cgrextend  31285  btwnexch2  31300  colineardim1  31338  lineext  31353  btwnconn1lem13  31376  btwnconn1lem14  31377  seglecgr12im  31387  outsideofeq  31407  outsideofeu  31408  nn0prpwlem  31487  neibastop2lem  31525  tailfb  31542  nndivsub  31626  ee7.2aOLD  31630  poimirlem31  32610  heicant  32614  filbcmb  32705  prdsbnd2  32764  heibor  32790  rngoisocnv  32950  ax12eq  33244  ax12el  33245  pmodlem2  34151  cdleme22b  34647  cdleme32d  34750  cdleme32f  34752  trlord  34875  cdlemj2  35128  cdlemk38  35221  cdlemk19x  35249  dihord2pre  35532  mzpcompact2lem  36332  pellfundex  36468  acongsym  36561  pwssplit4  36677  pwslnm  36682  relexpmulg  37021  stoweidlem17  38910  iccpartigtl  39961  fmtnofac2lem  40018  2pwp1prmfmtno  40042  lighneallem4  40065  bgoldbtbndlem2  40222  bgoldbtbndlem3  40223  bgoldbtbnd  40225  pfxccat3  40289  uhgr1wlkspthlem2  40960  crctcsh1wlkn0  41024  wwlksnred  41098  wwlksnextinj  41105  wspthsnwspthsnon  41122  umgr2wlk  41156  elwwlks2  41170  clwlkclwwlklem2a  41207  wwlksext2clwwlk  41231  eupth2lems  41406  frgrwopreglem2  41482  av-clwwlkextfrlem1  41509  av-frgraregord013  41549  lmod0rng  41658  2zrngamgm  41729