Theorem exp32 421

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

Syntax hints:   → wi 4   ∧ wa 396

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 208  df-an 397

This theorem is referenced by:  exp44  438  exp45  439  expr  457  anassrs  468  an13s  657  3impb  1120  wereu  5621  f0rn0  6719  funfvima3  7187  dff14i  7210  isomin  7288  isoini  7289  ovg  7528  elovmpt3rab1  7623  onint  7740  peano5  7840  poseq  8105  tfrlem11  8324  tz7.48lem  8377  oalimcl  8492  oaass  8493  resixpfo  8881  fundmen  8975  ssfiALT  9105  php3  9140  fodomfi  9219  fodomfiOLD  9237  marypha1lem  9343  card2inf  9467  ixpiunwdom  9502  cantnflt  9591  cnfcom  9619  dfac3  10041  dfac5lem5  10047  dfac5  10049  cfcoflem  10192  fin1a2s  10334  zorn2lem4  10419  zorn2lem7  10422  fpwwe2lem11  10562  wunfi  10642  grur1a  10740  addcanpi  10820  mulcanpi  10821  distrlem1pr  10946  ltaddpr  10955  ltexprlem1  10957  ltexprlem6  10962  ltexprlem7  10963  prodgt0  12000  mulgt1OLD  12012  uzwo  12859  xmulasslem  13235  xlemul1a  13238  faclbnd  14250  swrdwrdsymb  14623  pfxccatin12lem2a  14687  pfxccat3  14694  swrdccat  14695  cshwidxmod  14763  s3iunsndisj  14928  dvdsaddre2b  16274  divgcdcoprm0  16632  cncongr2  16635  infpnlem1  16879  isacs4lem  18508  cycsubm  19175  gsmsymgrfixlem1  19400  gsmsymgrfix  19401  imasabl  19849  dmdprdsplit2lem  20020  pgpfac1  20055  pgpfac  20059  lssssr  20951  islmhm2  21035  lspdisj  21125  pzriprnglem5  21467  pzriprnglem8  21470  cygznlem2a  21549  lindfmm  21809  scmataddcl  22506  scmatsubcl  22507  scmatmulcl  22508  cpmatacl  22706  cayhamlem3  22877  cayleyhamilton1  22882  neindisj  23107  cnpnei  23254  t0dist  23315  ordthauslem  23373  uncmp  23393  fiuncmp  23394  iunconnlem  23417  fbasrn  23874  rnelfmlem  23942  rnelfm  23943  fmfnfmlem2  23945  fmfnfmlem4  23947  fclscf  24015  alexsubALTlem3  24039  alexsubALTlem4  24040  alexsubALT  24041  reconn  24819  fsumcn  24862  ovolfiniun  25493  dyadmax  25590  dyadmbllem  25591  dvmptfsum  25967  dvlip2  25987  dvivthlem1  26000  dvcnvrelem1  26009  ply1divex  26127  fta1g  26160  plydivex  26288  fta1  26299  mulcxp  26674  zabsle1  27284  lgsquad2lem2  27373  2lgsoddprm  27404  pntlem3  27597  nodenselem8  27680  nocvxmin  27772  precsexlem11  28234  om2noseqrdg  28321  expadds  28452  brbtwn  28993  brcgr  28994  brbtwn2  28999  axeuclid  29057  finsumvtxdg2size  29644  uhgrwkspthlem2  29847  crctcshwlkn0  29914  wwlksnred  29985  wwlksnextinj  29992  umgr2wlk  30042  elwwlks2  30062  clwlkclwwlklem2a  30093  clwlkclwwlkf1lem3  30101  eupth2lems  30333  numclwwlk2lem1lem  30437  frgrregord013  30490  grpoidinvlem3  30602  shorth  31391  pjhthmo  31398  pjpjpre  31515  elspansn5  31670  lnopmi  32096  adjlnop  32182  leopmul2i  32231  stlesi  32337  ssmd2  32408  dmdsl3  32411  mdexchi  32431  cvexchlem  32464  atcv1  32476  atcvatlem  32481  atabsi  32497  mdsymlem2  32500  mdsymlem5  32503  sumdmdii  32511  sumdmdlem  32514  sumdmdlem2  32515  dya2iocnrect  34472  bnj571  35095  pconnconn  35466  iccllysconn  35485  satffunlem2lem1  35639  cgrextend  36243  btwnexch2  36258  colineardim1  36296  lineext  36311  btwnconn1lem13  36334  btwnconn1lem14  36335  seglecgr12im  36345  outsideofeq  36365  outsideofeu  36366  nn0prpwlem  36557  neibastop2lem  36595  tailfb  36612  nndivsub  36692  ee7.2aOLD  36696  fvineqsneu  37780  poimirlem31  38025  heicant  38029  filbcmb  38114  prdsbnd2  38169  heibor  38195  rngoisocnv  38355  ax12eq  39440  ax12el  39441  pmodlem2  40346  cdleme22b  40840  cdleme32d  40943  cdleme32f  40945  trlord  41068  cdlemj2  41321  cdlemk38  41414  cdlemk19x  41442  dihord2pre  41724  fsuppind  43047  mzpcompact2lem  43207  pellfundex  43338  acongsym  43428  pwssplit4  43541  pwslnm  43546  cantnfresb  43776  relexpmulg  44161  relpmin  45403  stoweidlem17  46467  2reu8i  47583  imasetpreimafvbijlemf1  47886  iccpartigtl  47905  paireqne  47993  fmtnofac2lem  48053  2pwp1prmfmtno  48075  lighneallem4  48095  bgoldbtbndlem2  48304  bgoldbtbndlem3  48305  bgoldbtbnd  48307  grimco  48387  isuspgrimlem  48393  cycl3grtri  48445  isubgr3stgrlem6  48469  lmod0rng  48727  2zrngamgm  48743