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

This theorem is referenced by:  exp44  437  exp45  438  expr  456  anassrs  467  an13s  647  3impb  1113  wereu  5584  f0rn0  6655  funfvima3  7106  isomin  7201  isoini  7202  ovg  7428  elovmpt3rab1  7520  onint  7630  peano5  7727  peano5OLD  7728  tfrlem11  8203  tz7.48lem  8256  oalimcl  8367  oaass  8368  resixpfo  8698  fundmen  8791  ssfiALT  8922  php3  8959  php3OLD  8972  fodomfi  9053  marypha1lem  9153  card2inf  9275  ixpiunwdom  9310  cantnflt  9391  cnfcom  9419  trpredmintr  9461  dfac3  9861  dfac5lem5  9867  dfac5  9868  cfcoflem  10012  fin1a2s  10154  zorn2lem4  10239  zorn2lem7  10242  fpwwe2lem11  10381  wunfi  10461  grur1a  10559  addcanpi  10639  mulcanpi  10640  distrlem1pr  10765  ltaddpr  10774  ltexprlem1  10776  ltexprlem6  10781  ltexprlem7  10782  prodgt0  11805  mulgt1  11817  uzwo  12633  xmulasslem  13001  xlemul1a  13004  faclbnd  13985  swrdwrdsymb  14356  pfxccatin12lem2a  14421  pfxccat3  14428  swrdccat  14429  cshwidxmod  14497  s3iunsndisj  14660  dvdsaddre2b  15997  divgcdcoprm0  16351  cncongr2  16354  infpnlem1  16592  isacs4lem  18243  cycsubm  18802  gsmsymgrfixlem1  19016  gsmsymgrfix  19017  dmdprdsplit2lem  19629  pgpfac1  19664  pgpfac  19668  lssssr  20196  islmhm2  20281  lspdisj  20368  cygznlem2a  20756  lindfmm  21015  scmataddcl  21646  scmatsubcl  21647  scmatmulcl  21648  cpmatacl  21846  cayhamlem3  22017  cayleyhamilton1  22022  neindisj  22249  cnpnei  22396  t0dist  22457  ordthauslem  22515  uncmp  22535  fiuncmp  22536  iunconnlem  22559  fbasrn  23016  rnelfmlem  23084  rnelfm  23085  fmfnfmlem2  23087  fmfnfmlem4  23089  fclscf  23157  alexsubALTlem3  23181  alexsubALTlem4  23182  alexsubALT  23183  reconn  23972  fsumcn  24014  ovolfiniun  24646  dyadmax  24743  dyadmbllem  24744  dvmptfsum  25120  dvlip2  25140  dvivthlem1  25153  dvcnvrelem1  25162  ply1divex  25282  fta1g  25313  plydivex  25438  fta1  25449  mulcxp  25821  zabsle1  26425  lgsquad2lem2  26514  2lgsoddprm  26545  pntlem3  26738  brbtwn  27248  brcgr  27249  brbtwn2  27254  axeuclid  27312  finsumvtxdg2size  27898  uhgrwkspthlem2  28101  crctcshwlkn0  28165  wwlksnred  28236  wwlksnextinj  28243  umgr2wlk  28293  elwwlks2  28310  clwlkclwwlklem2a  28341  clwlkclwwlkf1lem3  28349  eupth2lems  28581  numclwwlk2lem1lem  28685  frgrregord013  28738  grpoidinvlem3  28847  shorth  29636  pjhthmo  29643  pjpjpre  29760  elspansn5  29915  lnopmi  30341  adjlnop  30427  leopmul2i  30476  stlesi  30582  ssmd2  30653  dmdsl3  30656  mdexchi  30676  cvexchlem  30709  atcv1  30721  atcvatlem  30726  atabsi  30742  mdsymlem2  30745  mdsymlem5  30748  sumdmdii  30756  sumdmdlem  30759  sumdmdlem2  30760  dya2iocnrect  32227  bnj571  32865  pconnconn  33172  iccllysconn  33191  satffunlem2lem1  33345  poseq  33781  nodenselem8  33873  nocvxmin  33952  cgrextend  34289  btwnexch2  34304  colineardim1  34342  lineext  34357  btwnconn1lem13  34380  btwnconn1lem14  34381  seglecgr12im  34391  outsideofeq  34411  outsideofeu  34412  nn0prpwlem  34490  neibastop2lem  34528  tailfb  34545  nndivsub  34625  ee7.2aOLD  34629  fvineqsneu  35561  poimirlem31  35787  heicant  35791  filbcmb  35877  prdsbnd2  35932  heibor  35958  rngoisocnv  36118  ax12eq  36934  ax12el  36935  pmodlem2  37840  cdleme22b  38334  cdleme32d  38437  cdleme32f  38439  trlord  38562  cdlemj2  38815  cdlemk38  38908  cdlemk19x  38936  dihord2pre  39218  fsuppind  40259  mzpcompact2lem  40553  pellfundex  40688  acongsym  40778  pwssplit4  40894  pwslnm  40899  relexpmulg  41271  stoweidlem17  43512  2reu8i  44556  imasetpreimafvbijlemf1  44808  iccpartigtl  44827  paireqne  44915  fmtnofac2lem  44972  2pwp1prmfmtno  44994  lighneallem4  45014  bgoldbtbndlem2  45210  bgoldbtbndlem3  45211  bgoldbtbnd  45213  lmod0rng  45378  2zrngamgm  45449