Theorem exp32 423

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

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  exp44  440  exp45  441  expr  459  anassrs  470  an13s  649  3impb  1111  wereu  5553  f0rn0  6566  funfvima3  7000  isomin  7092  isoini  7093  ovg  7315  elovmpt3rab1  7407  onint  7512  peano5  7607  tfrlem11  8026  tz7.48lem  8079  oalimcl  8188  oaass  8189  resixpfo  8502  fundmen  8585  php3  8705  ssfi  8740  fodomfi  8799  marypha1lem  8899  card2inf  9021  ixpiunwdom  9057  cantnflt  9137  cnfcom  9165  dfac3  9549  dfac5lem5  9555  dfac5  9556  cfcoflem  9696  fin1a2s  9838  zorn2lem4  9923  zorn2lem7  9926  fpwwe2lem12  10065  wunfi  10145  grur1a  10243  addcanpi  10323  mulcanpi  10324  distrlem1pr  10449  ltaddpr  10458  ltexprlem1  10460  ltexprlem6  10465  ltexprlem7  10466  prodgt0  11489  mulgt1  11501  uzwo  12314  xmulasslem  12681  xlemul1a  12684  faclbnd  13653  swrdwrdsymb  14026  pfxccatin12lem2a  14091  pfxccat3  14098  swrdccat  14099  cshwidxmod  14167  s3iunsndisj  14330  dvdsaddre2b  15659  divgcdcoprm0  16011  cncongr2  16014  infpnlem1  16248  isacs4lem  17780  cycsubm  18347  gsmsymgrfixlem1  18557  gsmsymgrfix  18558  dmdprdsplit2lem  19169  pgpfac1  19204  pgpfac  19208  lssssr  19727  islmhm2  19812  lspdisj  19899  cygznlem2a  20716  lindfmm  20973  scmataddcl  21127  scmatsubcl  21128  scmatmulcl  21129  cpmatacl  21326  cayhamlem3  21497  cayleyhamilton1  21502  neindisj  21727  cnpnei  21874  t0dist  21935  ordthauslem  21993  uncmp  22013  fiuncmp  22014  iunconnlem  22037  fbasrn  22494  rnelfmlem  22562  rnelfm  22563  fmfnfmlem2  22565  fmfnfmlem4  22567  fclscf  22635  alexsubALTlem3  22659  alexsubALTlem4  22660  alexsubALT  22661  reconn  23438  fsumcn  23480  ovolfiniun  24104  dyadmax  24201  dyadmbllem  24202  dvmptfsum  24574  dvlip2  24594  dvivthlem1  24607  dvcnvrelem1  24616  ply1divex  24732  fta1g  24763  plydivex  24888  fta1  24899  mulcxp  25270  zabsle1  25874  lgsquad2lem2  25963  2lgsoddprm  25994  pntlem3  26187  brbtwn  26687  brcgr  26688  brbtwn2  26693  axeuclid  26751  finsumvtxdg2size  27334  uhgrwkspthlem2  27537  crctcshwlkn0  27601  wwlksnred  27672  wwlksnextinj  27679  umgr2wlk  27730  elwwlks2  27747  clwlkclwwlklem2a  27778  clwlkclwwlkf1lem3  27786  eupth2lems  28019  numclwwlk2lem1lem  28123  frgrregord013  28176  grpoidinvlem3  28285  shorth  29074  pjhthmo  29081  pjpjpre  29198  elspansn5  29353  lnopmi  29779  adjlnop  29865  leopmul2i  29914  stlesi  30020  ssmd2  30091  dmdsl3  30094  mdexchi  30114  cvexchlem  30147  atcv1  30159  atcvatlem  30164  atabsi  30180  mdsymlem2  30183  mdsymlem5  30186  sumdmdii  30194  sumdmdlem  30197  sumdmdlem2  30198  dya2iocnrect  31541  bnj571  32180  pconnconn  32480  iccllysconn  32499  satffunlem2lem1  32653  trpredmintr  33072  poseq  33097  nodenselem8  33197  nocvxmin  33250  cgrextend  33471  btwnexch2  33486  colineardim1  33524  lineext  33539  btwnconn1lem13  33562  btwnconn1lem14  33563  seglecgr12im  33573  outsideofeq  33593  outsideofeu  33594  nn0prpwlem  33672  neibastop2lem  33710  tailfb  33727  nndivsub  33807  ee7.2aOLD  33811  fvineqsneu  34694  poimirlem31  34925  heicant  34929  filbcmb  35017  prdsbnd2  35075  heibor  35101  rngoisocnv  35261  ax12eq  36079  ax12el  36080  pmodlem2  36985  cdleme22b  37479  cdleme32d  37582  cdleme32f  37584  trlord  37707  cdlemj2  37960  cdlemk38  38053  cdlemk19x  38081  dihord2pre  38363  mzpcompact2lem  39355  pellfundex  39490  acongsym  39580  pwssplit4  39696  pwslnm  39701  relexpmulg  40062  stoweidlem17  42309  2reu8i  43319  imasetpreimafvbijlemf1  43571  iccpartigtl  43590  paireqne  43680  fmtnofac2lem  43737  2pwp1prmfmtno  43759  lighneallem4  43782  bgoldbtbndlem2  43978  bgoldbtbndlem3  43979  bgoldbtbnd  43981  lmod0rng  44146  2zrngamgm  44217