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

This theorem is referenced by:  exp44  441  exp45  442  expr  460  anassrs  471  an13s  650  3impb  1112  wereu  5515  f0rn0  6538  funfvima3  6976  isomin  7069  isoini  7070  ovg  7293  elovmpt3rab1  7385  onint  7490  peano5  7585  tfrlem11  8007  tz7.48lem  8060  oalimcl  8169  oaass  8170  resixpfo  8483  fundmen  8566  php3  8687  ssfi  8722  fodomfi  8781  marypha1lem  8881  card2inf  9003  ixpiunwdom  9038  cantnflt  9119  cnfcom  9147  dfac3  9532  dfac5lem5  9538  dfac5  9539  cfcoflem  9683  fin1a2s  9825  zorn2lem4  9910  zorn2lem7  9913  fpwwe2lem12  10052  wunfi  10132  grur1a  10230  addcanpi  10310  mulcanpi  10311  distrlem1pr  10436  ltaddpr  10445  ltexprlem1  10447  ltexprlem6  10452  ltexprlem7  10453  prodgt0  11476  mulgt1  11488  uzwo  12299  xmulasslem  12666  xlemul1a  12669  faclbnd  13646  swrdwrdsymb  14015  pfxccatin12lem2a  14080  pfxccat3  14087  swrdccat  14088  cshwidxmod  14156  s3iunsndisj  14319  dvdsaddre2b  15649  divgcdcoprm0  15999  cncongr2  16002  infpnlem1  16236  isacs4lem  17770  cycsubm  18337  gsmsymgrfixlem1  18547  gsmsymgrfix  18548  dmdprdsplit2lem  19160  pgpfac1  19195  pgpfac  19199  lssssr  19718  islmhm2  19803  lspdisj  19890  cygznlem2a  20259  lindfmm  20516  scmataddcl  21121  scmatsubcl  21122  scmatmulcl  21123  cpmatacl  21321  cayhamlem3  21492  cayleyhamilton1  21497  neindisj  21722  cnpnei  21869  t0dist  21930  ordthauslem  21988  uncmp  22008  fiuncmp  22009  iunconnlem  22032  fbasrn  22489  rnelfmlem  22557  rnelfm  22558  fmfnfmlem2  22560  fmfnfmlem4  22562  fclscf  22630  alexsubALTlem3  22654  alexsubALTlem4  22655  alexsubALT  22656  reconn  23433  fsumcn  23475  ovolfiniun  24105  dyadmax  24202  dyadmbllem  24203  dvmptfsum  24578  dvlip2  24598  dvivthlem1  24611  dvcnvrelem1  24620  ply1divex  24737  fta1g  24768  plydivex  24893  fta1  24904  mulcxp  25276  zabsle1  25880  lgsquad2lem2  25969  2lgsoddprm  26000  pntlem3  26193  brbtwn  26693  brcgr  26694  brbtwn2  26699  axeuclid  26757  finsumvtxdg2size  27340  uhgrwkspthlem2  27543  crctcshwlkn0  27607  wwlksnred  27678  wwlksnextinj  27685  umgr2wlk  27735  elwwlks2  27752  clwlkclwwlklem2a  27783  clwlkclwwlkf1lem3  27791  eupth2lems  28023  numclwwlk2lem1lem  28127  frgrregord013  28180  grpoidinvlem3  28289  shorth  29078  pjhthmo  29085  pjpjpre  29202  elspansn5  29357  lnopmi  29783  adjlnop  29869  leopmul2i  29918  stlesi  30024  ssmd2  30095  dmdsl3  30098  mdexchi  30118  cvexchlem  30151  atcv1  30163  atcvatlem  30168  atabsi  30184  mdsymlem2  30187  mdsymlem5  30190  sumdmdii  30198  sumdmdlem  30201  sumdmdlem2  30202  dya2iocnrect  31649  bnj571  32288  pconnconn  32591  iccllysconn  32610  satffunlem2lem1  32764  trpredmintr  33183  poseq  33208  nodenselem8  33308  nocvxmin  33361  cgrextend  33582  btwnexch2  33597  colineardim1  33635  lineext  33650  btwnconn1lem13  33673  btwnconn1lem14  33674  seglecgr12im  33684  outsideofeq  33704  outsideofeu  33705  nn0prpwlem  33783  neibastop2lem  33821  tailfb  33838  nndivsub  33918  ee7.2aOLD  33922  fvineqsneu  34828  poimirlem31  35088  heicant  35092  filbcmb  35178  prdsbnd2  35233  heibor  35259  rngoisocnv  35419  ax12eq  36237  ax12el  36238  pmodlem2  37143  cdleme22b  37637  cdleme32d  37740  cdleme32f  37742  trlord  37865  cdlemj2  38118  cdlemk38  38211  cdlemk19x  38239  dihord2pre  38521  fsuppind  39456  mzpcompact2lem  39692  pellfundex  39827  acongsym  39917  pwssplit4  40033  pwslnm  40038  relexpmulg  40411  stoweidlem17  42659  2reu8i  43669  imasetpreimafvbijlemf1  43921  iccpartigtl  43940  paireqne  44028  fmtnofac2lem  44085  2pwp1prmfmtno  44107  lighneallem4  44128  bgoldbtbndlem2  44324  bgoldbtbndlem3  44325  bgoldbtbnd  44327  lmod0rng  44492  2zrngamgm  44563