Theorem exp32 422

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

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  exp44  439  exp45  440  expr  458  anassrs  469  an13s  650  3impb  1116  wereu  5673  f0rn0  6777  funfvima3  7238  isomin  7334  isoini  7335  ovg  7572  elovmpt3rab1  7666  onint  7778  peano5  7884  peano5OLD  7885  poseq  8144  tfrlem11  8388  tz7.48lem  8441  oalimcl  8560  oaass  8561  resixpfo  8930  fundmen  9031  ssfiALT  9174  php3  9212  php3OLD  9224  fodomfi  9325  marypha1lem  9428  card2inf  9550  ixpiunwdom  9585  cantnflt  9667  cnfcom  9695  dfac3  10116  dfac5lem5  10122  dfac5  10123  cfcoflem  10267  fin1a2s  10409  zorn2lem4  10494  zorn2lem7  10497  fpwwe2lem11  10636  wunfi  10716  grur1a  10814  addcanpi  10894  mulcanpi  10895  distrlem1pr  11020  ltaddpr  11029  ltexprlem1  11031  ltexprlem6  11036  ltexprlem7  11037  prodgt0  12061  mulgt1  12073  uzwo  12895  xmulasslem  13264  xlemul1a  13267  faclbnd  14250  swrdwrdsymb  14612  pfxccatin12lem2a  14677  pfxccat3  14684  swrdccat  14685  cshwidxmod  14753  s3iunsndisj  14915  dvdsaddre2b  16250  divgcdcoprm0  16602  cncongr2  16605  infpnlem1  16843  isacs4lem  18497  cycsubm  19079  gsmsymgrfixlem1  19295  gsmsymgrfix  19296  imasabl  19744  dmdprdsplit2lem  19915  pgpfac1  19950  pgpfac  19954  lssssr  20564  islmhm2  20649  lspdisj  20738  cygznlem2a  21123  lindfmm  21382  scmataddcl  22018  scmatsubcl  22019  scmatmulcl  22020  cpmatacl  22218  cayhamlem3  22389  cayleyhamilton1  22394  neindisj  22621  cnpnei  22768  t0dist  22829  ordthauslem  22887  uncmp  22907  fiuncmp  22908  iunconnlem  22931  fbasrn  23388  rnelfmlem  23456  rnelfm  23457  fmfnfmlem2  23459  fmfnfmlem4  23461  fclscf  23529  alexsubALTlem3  23553  alexsubALTlem4  23554  alexsubALT  23555  reconn  24344  fsumcn  24386  ovolfiniun  25018  dyadmax  25115  dyadmbllem  25116  dvmptfsum  25492  dvlip2  25512  dvivthlem1  25525  dvcnvrelem1  25534  ply1divex  25654  fta1g  25685  plydivex  25810  fta1  25821  mulcxp  26193  zabsle1  26799  lgsquad2lem2  26888  2lgsoddprm  26919  pntlem3  27112  nodenselem8  27194  nocvxmin  27280  precsexlem11  27663  brbtwn  28157  brcgr  28158  brbtwn2  28163  axeuclid  28221  finsumvtxdg2size  28807  uhgrwkspthlem2  29011  crctcshwlkn0  29075  wwlksnred  29146  wwlksnextinj  29153  umgr2wlk  29203  elwwlks2  29220  clwlkclwwlklem2a  29251  clwlkclwwlkf1lem3  29259  eupth2lems  29491  numclwwlk2lem1lem  29595  frgrregord013  29648  grpoidinvlem3  29759  shorth  30548  pjhthmo  30555  pjpjpre  30672  elspansn5  30827  lnopmi  31253  adjlnop  31339  leopmul2i  31388  stlesi  31494  ssmd2  31565  dmdsl3  31568  mdexchi  31588  cvexchlem  31621  atcv1  31633  atcvatlem  31638  atabsi  31654  mdsymlem2  31657  mdsymlem5  31660  sumdmdii  31668  sumdmdlem  31671  sumdmdlem2  31672  dya2iocnrect  33280  bnj571  33917  pconnconn  34222  iccllysconn  34241  satffunlem2lem1  34395  cgrextend  34980  btwnexch2  34995  colineardim1  35033  lineext  35048  btwnconn1lem13  35071  btwnconn1lem14  35072  seglecgr12im  35082  outsideofeq  35102  outsideofeu  35103  nn0prpwlem  35207  neibastop2lem  35245  tailfb  35262  nndivsub  35342  ee7.2aOLD  35346  fvineqsneu  36292  poimirlem31  36519  heicant  36523  filbcmb  36608  prdsbnd2  36663  heibor  36689  rngoisocnv  36849  ax12eq  37811  ax12el  37812  pmodlem2  38718  cdleme22b  39212  cdleme32d  39315  cdleme32f  39317  trlord  39440  cdlemj2  39693  cdlemk38  39786  cdlemk19x  39814  dihord2pre  40096  fsuppind  41162  mzpcompact2lem  41489  pellfundex  41624  acongsym  41715  pwssplit4  41831  pwslnm  41836  cantnfresb  42074  relexpmulg  42461  stoweidlem17  44733  2reu8i  45821  imasetpreimafvbijlemf1  46072  iccpartigtl  46091  paireqne  46179  fmtnofac2lem  46236  2pwp1prmfmtno  46258  lighneallem4  46278  bgoldbtbndlem2  46474  bgoldbtbndlem3  46475  bgoldbtbnd  46477  lmod0rng  46642  pzriprnglem5  46809  pzriprnglem8  46812  2zrngamgm  46837