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  651  3impb  1114  wereu  5615  f0rn0  6713  funfvima3  7176  dff14i  7199  isomin  7277  isoini  7278  ovg  7517  elovmpt3rab1  7612  onint  7729  peano5  7829  poseq  8094  tfrlem11  8313  tz7.48lem  8366  oalimcl  8481  oaass  8482  resixpfo  8866  fundmen  8960  ssfiALT  9090  php3  9125  fodomfi  9203  fodomfiOLD  9221  marypha1lem  9324  card2inf  9448  ixpiunwdom  9483  cantnflt  9569  cnfcom  9597  dfac3  10019  dfac5lem5  10025  dfac5  10027  cfcoflem  10170  fin1a2s  10312  zorn2lem4  10397  zorn2lem7  10400  fpwwe2lem11  10539  wunfi  10619  grur1a  10717  addcanpi  10797  mulcanpi  10798  distrlem1pr  10923  ltaddpr  10932  ltexprlem1  10934  ltexprlem6  10939  ltexprlem7  10940  prodgt0  11975  mulgt1OLD  11987  uzwo  12811  xmulasslem  13186  xlemul1a  13189  faclbnd  14199  swrdwrdsymb  14572  pfxccatin12lem2a  14636  pfxccat3  14643  swrdccat  14644  cshwidxmod  14712  s3iunsndisj  14877  dvdsaddre2b  16220  divgcdcoprm0  16578  cncongr2  16581  infpnlem1  16824  isacs4lem  18452  cycsubm  19116  gsmsymgrfixlem1  19341  gsmsymgrfix  19342  imasabl  19790  dmdprdsplit2lem  19961  pgpfac1  19996  pgpfac  20000  lssssr  20889  islmhm2  20974  lspdisj  21064  pzriprnglem5  21424  pzriprnglem8  21427  cygznlem2a  21506  lindfmm  21766  scmataddcl  22432  scmatsubcl  22433  scmatmulcl  22434  cpmatacl  22632  cayhamlem3  22803  cayleyhamilton1  22808  neindisj  23033  cnpnei  23180  t0dist  23241  ordthauslem  23299  uncmp  23319  fiuncmp  23320  iunconnlem  23343  fbasrn  23800  rnelfmlem  23868  rnelfm  23869  fmfnfmlem2  23871  fmfnfmlem4  23873  fclscf  23941  alexsubALTlem3  23965  alexsubALTlem4  23966  alexsubALT  23967  reconn  24745  fsumcn  24789  ovolfiniun  25430  dyadmax  25527  dyadmbllem  25528  dvmptfsum  25907  dvlip2  25928  dvivthlem1  25941  dvcnvrelem1  25950  ply1divex  26070  fta1g  26103  plydivex  26233  fta1  26244  mulcxp  26622  zabsle1  27235  lgsquad2lem2  27324  2lgsoddprm  27355  pntlem3  27548  nodenselem8  27631  nocvxmin  27719  precsexlem11  28156  om2noseqrdg  28235  expadds  28359  brbtwn  28879  brcgr  28880  brbtwn2  28885  axeuclid  28943  finsumvtxdg2size  29531  uhgrwkspthlem2  29734  crctcshwlkn0  29801  wwlksnred  29872  wwlksnextinj  29879  umgr2wlk  29929  elwwlks2  29949  clwlkclwwlklem2a  29980  clwlkclwwlkf1lem3  29988  eupth2lems  30220  numclwwlk2lem1lem  30324  frgrregord013  30377  grpoidinvlem3  30488  shorth  31277  pjhthmo  31284  pjpjpre  31401  elspansn5  31556  lnopmi  31982  adjlnop  32068  leopmul2i  32117  stlesi  32223  ssmd2  32294  dmdsl3  32297  mdexchi  32317  cvexchlem  32350  atcv1  32362  atcvatlem  32367  atabsi  32383  mdsymlem2  32386  mdsymlem5  32389  sumdmdii  32397  sumdmdlem  32400  sumdmdlem2  32401  dya2iocnrect  34315  bnj571  34939  pconnconn  35296  iccllysconn  35315  satffunlem2lem1  35469  cgrextend  36073  btwnexch2  36088  colineardim1  36126  lineext  36141  btwnconn1lem13  36164  btwnconn1lem14  36165  seglecgr12im  36175  outsideofeq  36195  outsideofeu  36196  nn0prpwlem  36387  neibastop2lem  36425  tailfb  36442  nndivsub  36522  ee7.2aOLD  36526  fvineqsneu  37476  poimirlem31  37711  heicant  37715  filbcmb  37800  prdsbnd2  37855  heibor  37881  rngoisocnv  38041  ax12eq  39060  ax12el  39061  pmodlem2  39966  cdleme22b  40460  cdleme32d  40563  cdleme32f  40565  trlord  40688  cdlemj2  40941  cdlemk38  41034  cdlemk19x  41062  dihord2pre  41344  fsuppind  42708  mzpcompact2lem  42868  pellfundex  43003  acongsym  43093  pwssplit4  43206  pwslnm  43211  cantnfresb  43441  relexpmulg  43827  relpmin  45069  stoweidlem17  46139  2reu8i  47237  imasetpreimafvbijlemf1  47528  iccpartigtl  47547  paireqne  47635  fmtnofac2lem  47692  2pwp1prmfmtno  47714  lighneallem4  47734  bgoldbtbndlem2  47930  bgoldbtbndlem3  47931  bgoldbtbnd  47933  grimco  48013  isuspgrimlem  48019  cycl3grtri  48071  isubgr3stgrlem6  48095  lmod0rng  48353  2zrngamgm  48369