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

This theorem is referenced by:  exp44  441  exp45  442  expr  460  anassrs  471  an13s  661  3impb  1126  wereu  5641  f0rn0  6745  funfvima3  7216  dff14i  7239  isomin  7317  isoini  7318  ovg  7557  elovmpt3rab1  7652  onint  7769  peano5  7870  poseq  8133  tfrlem11  8354  tz7.48lem  8407  oalimcl  8524  oaass  8525  resixpfo  8914  fundmen  9008  ssfiALT  9138  php3  9173  fodomfi  9252  fodomfiOLD  9270  marypha1lem  9376  card2inf  9500  ixpiunwdom  9535  cantnflt  9624  cnfcom  9652  dfac3  10074  dfac5lem5  10080  dfac5  10082  cfcoflem  10226  fin1a2s  10368  zorn2lem4  10453  zorn2lem7  10456  fpwwe2lem11  10596  wunfi  10676  grur1a  10774  addcanpi  10854  mulcanpi  10855  distrlem1pr  10980  ltaddpr  10989  ltexprlem1  10991  ltexprlem6  10996  ltexprlem7  10997  prodgt0  12035  mulgt1OLD  12047  uzwo  12909  xmulasslem  13285  xlemul1a  13288  faclbnd  14300  swrdwrdsymb  14673  pfxccatin12lem2a  14737  pfxccat3  14744  swrdccat  14745  cshwidxmod  14813  s3iunsndisj  14978  dvdsaddre2b  16324  divgcdcoprm0  16682  cncongr2  16685  infpnlem1  16929  isacs4lem  18559  cycsubm  19226  gsmsymgrfixlem1  19450  gsmsymgrfix  19451  imasabl  19899  dmdprdsplit2lem  20070  pgpfac1  20105  pgpfac  20109  lssssr  21001  islmhm2  21085  lspdisj  21175  pzriprnglem5  21517  pzriprnglem8  21520  cygznlem2a  21599  lindfmm  21859  scmataddcl  22556  scmatsubcl  22557  scmatmulcl  22558  cpmatacl  22756  cayhamlem3  22927  cayleyhamilton1  22932  neindisj  23157  cnpnei  23304  t0dist  23365  ordthauslem  23423  uncmp  23443  fiuncmp  23444  iunconnlem  23467  fbasrn  23924  rnelfmlem  23992  rnelfm  23993  fmfnfmlem2  23995  fmfnfmlem4  23997  fclscf  24065  alexsubALTlem3  24089  alexsubALTlem4  24090  alexsubALT  24091  reconn  24869  fsumcn  24912  ovolfiniun  25543  dyadmax  25640  dyadmbllem  25641  dvmptfsum  26017  dvlip2  26037  dvivthlem1  26050  dvcnvrelem1  26059  ply1divex  26177  fta1g  26210  plydivex  26338  fta1  26349  mulcxp  26727  zabsle1  27337  lgsquad2lem2  27426  2lgsoddprm  27457  pntlem3  27650  nodenselem8  27732  nocvxmin  27825  precsexlem11  28287  om2noseqrdg  28374  expadds  28505  brbtwn  29046  brcgr  29047  brbtwn2  29052  axeuclid  29110  finsumvtxdg2size  29697  uhgrwkspthlem2  29900  crctcshwlkn0  29967  wwlksnred  30038  wwlksnextinj  30045  umgr2wlk  30095  elwwlks2  30115  clwlkclwwlklem2a  30146  clwlkclwwlkf1lem3  30154  eupth2lems  30386  numclwwlk2lem1lem  30490  frgrregord013  30543  grpoidinvlem3  30655  shorth  31444  pjhthmo  31451  pjpjpre  31568  elspansn5  31723  lnopmi  32149  adjlnop  32235  leopmul2i  32284  stlesi  32390  ssmd2  32461  dmdsl3  32464  mdexchi  32484  cvexchlem  32517  atcv1  32529  atcvatlem  32534  atabsi  32550  mdsymlem2  32553  mdsymlem5  32556  sumdmdii  32564  sumdmdlem  32567  sumdmdlem2  32568  dya2iocnrect  34539  bnj571  35165  pconnconn  35545  iccllysconn  35564  satffunlem2lem1  35718  cgrextend  36322  btwnexch2  36337  colineardim1  36375  lineext  36390  btwnconn1lem13  36413  btwnconn1lem14  36414  seglecgr12im  36424  outsideofeq  36444  outsideofeu  36445  nn0prpwlem  36646  neibastop2lem  36684  tailfb  36701  nndivsub  36781  ee7.2aOLD  36785  fvineqsneu  37869  poimirlem31  38114  heicant  38118  filbcmb  38203  prdsbnd2  38258  heibor  38284  rngoisocnv  38444  ax12eq  39529  ax12el  39530  pmodlem2  40435  cdleme22b  40929  cdleme32d  41032  cdleme32f  41034  trlord  41157  cdlemj2  41410  cdlemk38  41503  cdlemk19x  41531  dihord2pre  41813  fsuppind  43136  mzpcompact2lem  43296  pellfundex  43427  acongsym  43517  pwssplit4  43630  pwslnm  43635  cantnfresb  43865  relexpmulg  44250  relpmin  45492  stoweidlem17  46555  2reu8i  47671  imasetpreimafvbijlemf1  47974  iccpartigtl  47993  paireqne  48081  fmtnofac2lem  48141  2pwp1prmfmtno  48163  lighneallem4  48183  bgoldbtbndlem2  48392  bgoldbtbndlem3  48393  bgoldbtbnd  48395  grimco  48475  isuspgrimlem  48481  cycl3grtri  48533  isubgr3stgrlem6  48557  lmod0rng  48815  2zrngamgm  48831