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  5618  f0rn0  6717  funfvima3  7182  dff14i  7205  isomin  7283  isoini  7284  ovg  7523  elovmpt3rab1  7618  onint  7735  peano5  7835  poseq  8099  tfrlem11  8318  tz7.48lem  8371  oalimcl  8486  oaass  8487  resixpfo  8875  fundmen  8969  ssfiALT  9099  php3  9134  fodomfi  9213  fodomfiOLD  9231  marypha1lem  9337  card2inf  9461  ixpiunwdom  9496  cantnflt  9582  cnfcom  9610  dfac3  10032  dfac5lem5  10038  dfac5  10040  cfcoflem  10183  fin1a2s  10325  zorn2lem4  10410  zorn2lem7  10413  fpwwe2lem11  10553  wunfi  10633  grur1a  10731  addcanpi  10811  mulcanpi  10812  distrlem1pr  10937  ltaddpr  10946  ltexprlem1  10948  ltexprlem6  10953  ltexprlem7  10954  prodgt0  11989  mulgt1OLD  12001  uzwo  12825  xmulasslem  13201  xlemul1a  13204  faclbnd  14214  swrdwrdsymb  14587  pfxccatin12lem2a  14651  pfxccat3  14658  swrdccat  14659  cshwidxmod  14727  s3iunsndisj  14892  dvdsaddre2b  16235  divgcdcoprm0  16593  cncongr2  16596  infpnlem1  16839  isacs4lem  18468  cycsubm  19135  gsmsymgrfixlem1  19360  gsmsymgrfix  19361  imasabl  19809  dmdprdsplit2lem  19980  pgpfac1  20015  pgpfac  20019  lssssr  20907  islmhm2  20992  lspdisj  21082  pzriprnglem5  21442  pzriprnglem8  21445  cygznlem2a  21524  lindfmm  21784  scmataddcl  22459  scmatsubcl  22460  scmatmulcl  22461  cpmatacl  22659  cayhamlem3  22830  cayleyhamilton1  22835  neindisj  23060  cnpnei  23207  t0dist  23268  ordthauslem  23326  uncmp  23346  fiuncmp  23347  iunconnlem  23370  fbasrn  23827  rnelfmlem  23895  rnelfm  23896  fmfnfmlem2  23898  fmfnfmlem4  23900  fclscf  23968  alexsubALTlem3  23992  alexsubALTlem4  23993  alexsubALT  23994  reconn  24772  fsumcn  24815  ovolfiniun  25446  dyadmax  25543  dyadmbllem  25544  dvmptfsum  25920  dvlip2  25941  dvivthlem1  25954  dvcnvrelem1  25963  ply1divex  26083  fta1g  26116  plydivex  26245  fta1  26256  mulcxp  26634  zabsle1  27247  lgsquad2lem2  27336  2lgsoddprm  27367  pntlem3  27560  nodenselem8  27643  nocvxmin  27735  precsexlem11  28197  om2noseqrdg  28284  expadds  28415  brbtwn  28956  brcgr  28957  brbtwn2  28962  axeuclid  29020  finsumvtxdg2size  29608  uhgrwkspthlem2  29811  crctcshwlkn0  29878  wwlksnred  29949  wwlksnextinj  29956  umgr2wlk  30006  elwwlks2  30026  clwlkclwwlklem2a  30057  clwlkclwwlkf1lem3  30065  eupth2lems  30297  numclwwlk2lem1lem  30401  frgrregord013  30454  grpoidinvlem3  30566  shorth  31355  pjhthmo  31362  pjpjpre  31479  elspansn5  31634  lnopmi  32060  adjlnop  32146  leopmul2i  32195  stlesi  32301  ssmd2  32372  dmdsl3  32375  mdexchi  32395  cvexchlem  32428  atcv1  32440  atcvatlem  32445  atabsi  32461  mdsymlem2  32464  mdsymlem5  32467  sumdmdii  32475  sumdmdlem  32478  sumdmdlem2  32479  dya2iocnrect  34431  bnj571  35054  pconnconn  35419  iccllysconn  35438  satffunlem2lem1  35592  cgrextend  36196  btwnexch2  36211  colineardim1  36249  lineext  36264  btwnconn1lem13  36287  btwnconn1lem14  36288  seglecgr12im  36298  outsideofeq  36318  outsideofeu  36319  nn0prpwlem  36510  neibastop2lem  36548  tailfb  36565  nndivsub  36645  ee7.2aOLD  36649  fvineqsneu  37723  poimirlem31  37963  heicant  37967  filbcmb  38052  prdsbnd2  38107  heibor  38133  rngoisocnv  38293  ax12eq  39378  ax12el  39379  pmodlem2  40284  cdleme22b  40778  cdleme32d  40881  cdleme32f  40883  trlord  41006  cdlemj2  41259  cdlemk38  41352  cdlemk19x  41380  dihord2pre  41662  fsuppind  43022  mzpcompact2lem  43182  pellfundex  43317  acongsym  43407  pwssplit4  43520  pwslnm  43525  cantnfresb  43755  relexpmulg  44140  relpmin  45382  stoweidlem17  46449  2reu8i  47547  imasetpreimafvbijlemf1  47838  iccpartigtl  47857  paireqne  47945  fmtnofac2lem  48002  2pwp1prmfmtno  48024  lighneallem4  48044  bgoldbtbndlem2  48240  bgoldbtbndlem3  48241  bgoldbtbnd  48243  grimco  48323  isuspgrimlem  48329  cycl3grtri  48381  isubgr3stgrlem6  48405  lmod0rng  48663  2zrngamgm  48679