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  5634  f0rn0  6745  funfvima3  7210  dff14i  7234  isomin  7312  isoini  7313  ovg  7554  elovmpt3rab1  7649  onint  7766  peano5  7869  poseq  8137  tfrlem11  8356  tz7.48lem  8409  oalimcl  8524  oaass  8525  resixpfo  8909  fundmen  9002  ssfiALT  9138  php3  9173  fodomfi  9261  fodomfiOLD  9281  marypha1lem  9384  card2inf  9508  ixpiunwdom  9543  cantnflt  9625  cnfcom  9653  dfac3  10074  dfac5lem5  10080  dfac5  10082  cfcoflem  10225  fin1a2s  10367  zorn2lem4  10452  zorn2lem7  10455  fpwwe2lem11  10594  wunfi  10674  grur1a  10772  addcanpi  10852  mulcanpi  10853  distrlem1pr  10978  ltaddpr  10987  ltexprlem1  10989  ltexprlem6  10994  ltexprlem7  10995  prodgt0  12029  mulgt1OLD  12041  uzwo  12870  xmulasslem  13245  xlemul1a  13248  faclbnd  14255  swrdwrdsymb  14627  pfxccatin12lem2a  14692  pfxccat3  14699  swrdccat  14700  cshwidxmod  14768  s3iunsndisj  14934  dvdsaddre2b  16277  divgcdcoprm0  16635  cncongr2  16638  infpnlem1  16881  isacs4lem  18503  cycsubm  19134  gsmsymgrfixlem1  19357  gsmsymgrfix  19358  imasabl  19806  dmdprdsplit2lem  19977  pgpfac1  20012  pgpfac  20016  lssssr  20860  islmhm2  20945  lspdisj  21035  pzriprnglem5  21395  pzriprnglem8  21398  cygznlem2a  21477  lindfmm  21736  scmataddcl  22403  scmatsubcl  22404  scmatmulcl  22405  cpmatacl  22603  cayhamlem3  22774  cayleyhamilton1  22779  neindisj  23004  cnpnei  23151  t0dist  23212  ordthauslem  23270  uncmp  23290  fiuncmp  23291  iunconnlem  23314  fbasrn  23771  rnelfmlem  23839  rnelfm  23840  fmfnfmlem2  23842  fmfnfmlem4  23844  fclscf  23912  alexsubALTlem3  23936  alexsubALTlem4  23937  alexsubALT  23938  reconn  24717  fsumcn  24761  ovolfiniun  25402  dyadmax  25499  dyadmbllem  25500  dvmptfsum  25879  dvlip2  25900  dvivthlem1  25913  dvcnvrelem1  25922  ply1divex  26042  fta1g  26075  plydivex  26205  fta1  26216  mulcxp  26594  zabsle1  27207  lgsquad2lem2  27296  2lgsoddprm  27327  pntlem3  27520  nodenselem8  27603  nocvxmin  27690  precsexlem11  28119  om2noseqrdg  28198  expadds  28320  brbtwn  28826  brcgr  28827  brbtwn2  28832  axeuclid  28890  finsumvtxdg2size  29478  uhgrwkspthlem2  29684  crctcshwlkn0  29751  wwlksnred  29822  wwlksnextinj  29829  umgr2wlk  29879  elwwlks2  29896  clwlkclwwlklem2a  29927  clwlkclwwlkf1lem3  29935  eupth2lems  30167  numclwwlk2lem1lem  30271  frgrregord013  30324  grpoidinvlem3  30435  shorth  31224  pjhthmo  31231  pjpjpre  31348  elspansn5  31503  lnopmi  31929  adjlnop  32015  leopmul2i  32064  stlesi  32170  ssmd2  32241  dmdsl3  32244  mdexchi  32264  cvexchlem  32297  atcv1  32309  atcvatlem  32314  atabsi  32330  mdsymlem2  32333  mdsymlem5  32336  sumdmdii  32344  sumdmdlem  32347  sumdmdlem2  32348  dya2iocnrect  34272  bnj571  34896  pconnconn  35218  iccllysconn  35237  satffunlem2lem1  35391  cgrextend  35996  btwnexch2  36011  colineardim1  36049  lineext  36064  btwnconn1lem13  36087  btwnconn1lem14  36088  seglecgr12im  36098  outsideofeq  36118  outsideofeu  36119  nn0prpwlem  36310  neibastop2lem  36348  tailfb  36365  nndivsub  36445  ee7.2aOLD  36449  fvineqsneu  37399  poimirlem31  37645  heicant  37649  filbcmb  37734  prdsbnd2  37789  heibor  37815  rngoisocnv  37975  ax12eq  38934  ax12el  38935  pmodlem2  39841  cdleme22b  40335  cdleme32d  40438  cdleme32f  40440  trlord  40563  cdlemj2  40816  cdlemk38  40909  cdlemk19x  40937  dihord2pre  41219  fsuppind  42578  mzpcompact2lem  42739  pellfundex  42874  acongsym  42965  pwssplit4  43078  pwslnm  43083  cantnfresb  43313  relexpmulg  43699  relpmin  44942  stoweidlem17  46015  2reu8i  47114  imasetpreimafvbijlemf1  47405  iccpartigtl  47424  paireqne  47512  fmtnofac2lem  47569  2pwp1prmfmtno  47591  lighneallem4  47611  bgoldbtbndlem2  47807  bgoldbtbndlem3  47808  bgoldbtbnd  47810  grimco  47889  isuspgrimlem  47895  cycl3grtri  47946  isubgr3stgrlem6  47970  lmod0rng  48217  2zrngamgm  48233