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  5620  f0rn0  6719  funfvima3  7182  dff14i  7205  isomin  7283  isoini  7284  ovg  7523  elovmpt3rab1  7618  onint  7735  peano5  7835  poseq  8100  tfrlem11  8319  tz7.48lem  8372  oalimcl  8487  oaass  8488  resixpfo  8874  fundmen  8968  ssfiALT  9098  php3  9133  fodomfi  9212  fodomfiOLD  9230  marypha1lem  9336  card2inf  9460  ixpiunwdom  9495  cantnflt  9581  cnfcom  9609  dfac3  10031  dfac5lem5  10037  dfac5  10039  cfcoflem  10182  fin1a2s  10324  zorn2lem4  10409  zorn2lem7  10412  fpwwe2lem11  10552  wunfi  10632  grur1a  10730  addcanpi  10810  mulcanpi  10811  distrlem1pr  10936  ltaddpr  10945  ltexprlem1  10947  ltexprlem6  10952  ltexprlem7  10953  prodgt0  11988  mulgt1OLD  12000  uzwo  12824  xmulasslem  13200  xlemul1a  13203  faclbnd  14213  swrdwrdsymb  14586  pfxccatin12lem2a  14650  pfxccat3  14657  swrdccat  14658  cshwidxmod  14726  s3iunsndisj  14891  dvdsaddre2b  16234  divgcdcoprm0  16592  cncongr2  16595  infpnlem1  16838  isacs4lem  18467  cycsubm  19131  gsmsymgrfixlem1  19356  gsmsymgrfix  19357  imasabl  19805  dmdprdsplit2lem  19976  pgpfac1  20011  pgpfac  20015  lssssr  20905  islmhm2  20990  lspdisj  21080  pzriprnglem5  21440  pzriprnglem8  21443  cygznlem2a  21522  lindfmm  21782  scmataddcl  22460  scmatsubcl  22461  scmatmulcl  22462  cpmatacl  22660  cayhamlem3  22831  cayleyhamilton1  22836  neindisj  23061  cnpnei  23208  t0dist  23269  ordthauslem  23327  uncmp  23347  fiuncmp  23348  iunconnlem  23371  fbasrn  23828  rnelfmlem  23896  rnelfm  23897  fmfnfmlem2  23899  fmfnfmlem4  23901  fclscf  23969  alexsubALTlem3  23993  alexsubALTlem4  23994  alexsubALT  23995  reconn  24773  fsumcn  24817  ovolfiniun  25458  dyadmax  25555  dyadmbllem  25556  dvmptfsum  25935  dvlip2  25956  dvivthlem1  25969  dvcnvrelem1  25978  ply1divex  26098  fta1g  26131  plydivex  26261  fta1  26272  mulcxp  26650  zabsle1  27263  lgsquad2lem2  27352  2lgsoddprm  27383  pntlem3  27576  nodenselem8  27659  nocvxmin  27751  precsexlem11  28213  om2noseqrdg  28300  expadds  28431  brbtwn  28972  brcgr  28973  brbtwn2  28978  axeuclid  29036  finsumvtxdg2size  29624  uhgrwkspthlem2  29827  crctcshwlkn0  29894  wwlksnred  29965  wwlksnextinj  29972  umgr2wlk  30022  elwwlks2  30042  clwlkclwwlklem2a  30073  clwlkclwwlkf1lem3  30081  eupth2lems  30313  numclwwlk2lem1lem  30417  frgrregord013  30470  grpoidinvlem3  30581  shorth  31370  pjhthmo  31377  pjpjpre  31494  elspansn5  31649  lnopmi  32075  adjlnop  32161  leopmul2i  32210  stlesi  32316  ssmd2  32387  dmdsl3  32390  mdexchi  32410  cvexchlem  32443  atcv1  32455  atcvatlem  32460  atabsi  32476  mdsymlem2  32479  mdsymlem5  32482  sumdmdii  32490  sumdmdlem  32493  sumdmdlem2  32494  dya2iocnrect  34438  bnj571  35062  pconnconn  35425  iccllysconn  35444  satffunlem2lem1  35598  cgrextend  36202  btwnexch2  36217  colineardim1  36255  lineext  36270  btwnconn1lem13  36293  btwnconn1lem14  36294  seglecgr12im  36304  outsideofeq  36324  outsideofeu  36325  nn0prpwlem  36516  neibastop2lem  36554  tailfb  36571  nndivsub  36651  ee7.2aOLD  36655  fvineqsneu  37612  poimirlem31  37848  heicant  37852  filbcmb  37937  prdsbnd2  37992  heibor  38018  rngoisocnv  38178  ax12eq  39197  ax12el  39198  pmodlem2  40103  cdleme22b  40597  cdleme32d  40700  cdleme32f  40702  trlord  40825  cdlemj2  41078  cdlemk38  41171  cdlemk19x  41199  dihord2pre  41481  fsuppind  42829  mzpcompact2lem  42989  pellfundex  43124  acongsym  43214  pwssplit4  43327  pwslnm  43332  cantnfresb  43562  relexpmulg  43947  relpmin  45189  stoweidlem17  46257  2reu8i  47355  imasetpreimafvbijlemf1  47646  iccpartigtl  47665  paireqne  47753  fmtnofac2lem  47810  2pwp1prmfmtno  47832  lighneallem4  47852  bgoldbtbndlem2  48048  bgoldbtbndlem3  48049  bgoldbtbnd  48051  grimco  48131  isuspgrimlem  48137  cycl3grtri  48189  isubgr3stgrlem6  48213  lmod0rng  48471  2zrngamgm  48487