Theorem exp32 425

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

Syntax hints:   → wi 4   ∧ wa 400

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 401

This theorem is referenced by:  exp44  442  exp45  443  expr  461  anassrs  472  an13s  663  3impb  1132  wereu  5659  f0rn0  6765  funfvima3  7236  dff14i  7259  isomin  7337  isoini  7338  ovg  7577  elovmpt3rab1  7672  onint  7790  peano5  7891  poseq  8155  tfrlem11  8376  tz7.48lem  8429  oalimcl  8546  oaass  8547  resixpfo  8935  fundmen  9029  ssfiALT  9159  php3  9194  fodomfi  9273  marypha1lem  9394  card2inf  9518  ixpiunwdom  9553  cantnflt  9642  cnfcom  9670  dfac3  10106  dfac5lem5  10112  dfac5  10113  cfcoflem  10257  fin1a2s  10399  zorn2lem4  10484  zorn2lem7  10487  fpwwe2lem11  10627  wunfi  10707  grur1a  10805  addcanpi  10885  mulcanpi  10886  distrlem1pr  11011  ltaddpr  11020  ltexprlem1  11022  ltexprlem6  11027  ltexprlem7  11028  prodgt0  12063  uzwo  12936  xmulasslem  13312  xlemul1a  13315  faclbnd  14328  swrdwrdsymb  14702  pfxccatin12lem2a  14766  pfxccat3  14773  swrdccat  14774  cshwidxmod  14842  s3iunsndisj  15007  dvdsaddre2b  16366  divgcdcoprm0  16724  cncongr2  16727  infpnlem1  16971  isacs4lem  18601  cycsubm  19274  gsmsymgrfixlem1  19498  gsmsymgrfix  19499  imasabl  19947  dmdprdsplit2lem  20118  pgpfac1  20153  pgpfac  20157  lssssr  21056  islmhm2  21140  lspdisj  21230  pzriprnglem5  21616  pzriprnglem8  21619  cygznlem2a  21698  lindfmm  21958  scmataddcl  22654  scmatsubcl  22655  scmatmulcl  22656  cpmatacl  22854  cayhamlem3  23025  cayleyhamilton1  23030  neindisj  23255  cnpnei  23402  t0dist  23463  ordthauslem  23521  uncmp  23541  fiuncmp  23542  iunconnlem  23565  fbasrn  24022  rnelfmlem  24090  rnelfm  24091  fmfnfmlem2  24093  fmfnfmlem4  24095  fclscf  24163  alexsubALTlem3  24187  alexsubALTlem4  24188  alexsubALT  24189  reconn  24967  fsumcn  25010  ovolfiniun  25641  dyadmax  25738  dyadmbllem  25739  dvmptfsum  26115  dvlip2  26135  dvivthlem1  26148  dvcnvrelem1  26157  ply1divex  26275  fta1g  26308  plydivex  26439  fta1  26450  mulcxp  26831  zabsle1  27441  lgsquad2lem2  27530  2lgsoddprm  27561  pntlem3  27754  nodenselem8  27836  nocvxmin  27929  precsexlem11  28391  om2noseqrdg  28478  expadds  28609  brbtwn  29230  brcgr  29231  brbtwn2  29236  axeuclid  29294  finsumvtxdg2size  29881  uhgrwkspthlem2  30084  crctcshwlkn0  30151  wwlksnred  30222  wwlksnextinj  30229  umgr2wlk  30279  elwwlks2  30299  clwlkclwwlklem2a  30330  clwlkclwwlkf1lem3  30338  eupth2lems  30570  numclwwlk2lem1lem  30674  frgrregord013  30727  grpoidinvlem3  30839  shorth  31628  pjhthmo  31635  pjpjpre  31752  elspansn5  31907  lnopmi  32333  adjlnop  32419  leopmul2i  32468  stlesi  32574  ssmd2  32645  dmdsl3  32648  mdexchi  32668  cvexchlem  32701  atcv1  32713  atcvatlem  32718  atabsi  32734  mdsymlem2  32737  mdsymlem5  32740  sumdmdii  32748  sumdmdlem  32751  sumdmdlem2  32752  dya2iocnrect  34652  bnj571  35275  pconnconn  35704  iccllysconn  35723  satffunlem2lem1  35877  cgrextend  36481  btwnexch2  36496  colineardim1  36534  lineext  36549  btwnconn1lem13  36572  btwnconn1lem14  36573  seglecgr12im  36583  outsideofeq  36603  outsideofeu  36604  nn0prpwlem  36814  neibastop2lem  36852  tailfb  36869  nndivsub  36949  ee7.2aOLD  36953  fvineqsneu  38038  poimirlem31  38283  heicant  38287  filbcmb  38372  prdsbnd2  38427  heibor  38453  rngoisocnv  38613  ax12eq  39696  ax12el  39697  pmodlem2  40602  cdleme22b  41096  cdleme32d  41199  cdleme32f  41201  trlord  41324  cdlemj2  41577  cdlemk38  41670  cdlemk19x  41698  dihord2pre  41980  fsuppind  43305  mzpcompact2lem  43465  pellfundex  43596  acongsym  43686  pwssplit4  43799  pwslnm  43804  cantnfresb  44034  relexpmulg  44419  relpmin  45644  stoweidlem17  46714  2reu8i  47833  imasetpreimafvbijlemf1  48136  iccpartigtl  48155  paireqne  48243  fmtnofac2lem  48303  2pwp1prmfmtno  48325  lighneallem4  48345  bgoldbtbndlem2  48554  bgoldbtbndlem3  48555  bgoldbtbnd  48557  grimco  48637  isuspgrimlem  48643  cycl3grtri  48695  isubgr3stgrlem6  48719  lmod0rng  48977  2zrngamgm  48993