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  5637  f0rn0  6748  funfvima3  7213  dff14i  7237  isomin  7315  isoini  7316  ovg  7557  elovmpt3rab1  7652  onint  7769  peano5  7872  poseq  8140  tfrlem11  8359  tz7.48lem  8412  oalimcl  8527  oaass  8528  resixpfo  8912  fundmen  9005  ssfiALT  9144  php3  9179  fodomfi  9268  fodomfiOLD  9288  marypha1lem  9391  card2inf  9515  ixpiunwdom  9550  cantnflt  9632  cnfcom  9660  dfac3  10081  dfac5lem5  10087  dfac5  10089  cfcoflem  10232  fin1a2s  10374  zorn2lem4  10459  zorn2lem7  10462  fpwwe2lem11  10601  wunfi  10681  grur1a  10779  addcanpi  10859  mulcanpi  10860  distrlem1pr  10985  ltaddpr  10994  ltexprlem1  10996  ltexprlem6  11001  ltexprlem7  11002  prodgt0  12036  mulgt1OLD  12048  uzwo  12877  xmulasslem  13252  xlemul1a  13255  faclbnd  14262  swrdwrdsymb  14634  pfxccatin12lem2a  14699  pfxccat3  14706  swrdccat  14707  cshwidxmod  14775  s3iunsndisj  14941  dvdsaddre2b  16284  divgcdcoprm0  16642  cncongr2  16645  infpnlem1  16888  isacs4lem  18510  cycsubm  19141  gsmsymgrfixlem1  19364  gsmsymgrfix  19365  imasabl  19813  dmdprdsplit2lem  19984  pgpfac1  20019  pgpfac  20023  lssssr  20867  islmhm2  20952  lspdisj  21042  pzriprnglem5  21402  pzriprnglem8  21405  cygznlem2a  21484  lindfmm  21743  scmataddcl  22410  scmatsubcl  22411  scmatmulcl  22412  cpmatacl  22610  cayhamlem3  22781  cayleyhamilton1  22786  neindisj  23011  cnpnei  23158  t0dist  23219  ordthauslem  23277  uncmp  23297  fiuncmp  23298  iunconnlem  23321  fbasrn  23778  rnelfmlem  23846  rnelfm  23847  fmfnfmlem2  23849  fmfnfmlem4  23851  fclscf  23919  alexsubALTlem3  23943  alexsubALTlem4  23944  alexsubALT  23945  reconn  24724  fsumcn  24768  ovolfiniun  25409  dyadmax  25506  dyadmbllem  25507  dvmptfsum  25886  dvlip2  25907  dvivthlem1  25920  dvcnvrelem1  25929  ply1divex  26049  fta1g  26082  plydivex  26212  fta1  26223  mulcxp  26601  zabsle1  27214  lgsquad2lem2  27303  2lgsoddprm  27334  pntlem3  27527  nodenselem8  27610  nocvxmin  27697  precsexlem11  28126  om2noseqrdg  28205  expadds  28327  brbtwn  28833  brcgr  28834  brbtwn2  28839  axeuclid  28897  finsumvtxdg2size  29485  uhgrwkspthlem2  29691  crctcshwlkn0  29758  wwlksnred  29829  wwlksnextinj  29836  umgr2wlk  29886  elwwlks2  29903  clwlkclwwlklem2a  29934  clwlkclwwlkf1lem3  29942  eupth2lems  30174  numclwwlk2lem1lem  30278  frgrregord013  30331  grpoidinvlem3  30442  shorth  31231  pjhthmo  31238  pjpjpre  31355  elspansn5  31510  lnopmi  31936  adjlnop  32022  leopmul2i  32071  stlesi  32177  ssmd2  32248  dmdsl3  32251  mdexchi  32271  cvexchlem  32304  atcv1  32316  atcvatlem  32321  atabsi  32337  mdsymlem2  32340  mdsymlem5  32343  sumdmdii  32351  sumdmdlem  32354  sumdmdlem2  32355  dya2iocnrect  34279  bnj571  34903  pconnconn  35225  iccllysconn  35244  satffunlem2lem1  35398  cgrextend  36003  btwnexch2  36018  colineardim1  36056  lineext  36071  btwnconn1lem13  36094  btwnconn1lem14  36095  seglecgr12im  36105  outsideofeq  36125  outsideofeu  36126  nn0prpwlem  36317  neibastop2lem  36355  tailfb  36372  nndivsub  36452  ee7.2aOLD  36456  fvineqsneu  37406  poimirlem31  37652  heicant  37656  filbcmb  37741  prdsbnd2  37796  heibor  37822  rngoisocnv  37982  ax12eq  38941  ax12el  38942  pmodlem2  39848  cdleme22b  40342  cdleme32d  40445  cdleme32f  40447  trlord  40570  cdlemj2  40823  cdlemk38  40916  cdlemk19x  40944  dihord2pre  41226  fsuppind  42585  mzpcompact2lem  42746  pellfundex  42881  acongsym  42972  pwssplit4  43085  pwslnm  43090  cantnfresb  43320  relexpmulg  43706  relpmin  44949  stoweidlem17  46022  2reu8i  47118  imasetpreimafvbijlemf1  47409  iccpartigtl  47428  paireqne  47516  fmtnofac2lem  47573  2pwp1prmfmtno  47595  lighneallem4  47615  bgoldbtbndlem2  47811  bgoldbtbndlem3  47812  bgoldbtbnd  47814  grimco  47893  isuspgrimlem  47899  cycl3grtri  47950  isubgr3stgrlem6  47974  lmod0rng  48221  2zrngamgm  48237