Theorem mp3an12 1452

Description: An inference based on modus ponens. (Contributed by NM, 13-Jul-2005.)

Hypotheses

Ref	Expression
mp3an12.1	⊢ 𝜑
mp3an12.2	⊢ 𝜓
mp3an12.3	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
mp3an12	⊢ (𝜒 → 𝜃)

Proof of Theorem mp3an12

Step	Hyp	Ref	Expression
1		mp3an12.2	. 2 ⊢ 𝜓
2		mp3an12.1	. . 3 ⊢ 𝜑
3		mp3an12.3	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
4	2, 3	mp3an1 1449	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 689	1 ⊢ (𝜒 → 𝜃)

Syntax hints:   → wi 4   ∧ w3a 1088

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 206  df-an 398  df-3an 1090

This theorem is referenced by:  mp3an12i  1466  ceqsalg  3508  ceqsralvOLD  3515  brelrn  5942  predeq3  6305  funpr  6605  fvpr1  7191  fvpr2  7193  tfi  7842  peano5  7884  peano5OLD  7885  wrecseq3  8305  wfr3OLD  8338  fpm  8869  0fsupp  9385  ssttrcl  9710  ac6  10475  alephadd  10572  axpre-sup  11164  cnegex2  11396  addlid  11397  renegcli  11521  div0  11902  divclzi  11949  divcan1zi  11950  divcan2zi  11951  divreczi  11952  divcan3zi  11953  divcan4zi  11954  divasszi  11964  divmulzi  11965  divdirzi  11966  redivclzi  11980  ltm1  12056  mulgt1  12073  recgt1i  12111  ltmul1i  12132  ltdiv1i  12133  ltmuldivi  12134  ltmul2i  12135  lemul1i  12136  lemul2i  12137  ledivp1i  12139  ltdivp1i  12140  nnge1  12240  nngt0  12243  nnrecgt0  12255  nnunb  12468  recnz  12637  eluzsubi  12855  ge0gtmnf  13151  x2times  13278  xrub  13291  xrge0neqmnf  13429  1mod  13868  m1expcl2  14051  1exp  14057  expubnd  14142  iexpcyc  14171  expnbnd  14195  expnlbnd  14196  faclbnd4lem1  14253  imval2  15098  cjdivi  15138  resqrex  15197  sqrtneglem  15213  absdivzi  15354  climcndslem1  15795  climcndslem2  15796  fprodge1  15939  bpoly3  16002  sinhval  16097  coshval  16098  ef01bndlem  16127  sin01gt0  16133  cos01gt0  16134  evend2  16300  divalglem5  16340  vdwlem13  16926  prmlem1  17041  prmlem2  17053  ress0  17188  frmdplusg  18735  m1expaddsub  19366  islindf4  21393  resstopn  22690  lecldbas  22723  hmphindis  23301  cnbl0  24290  xrsmopn  24328  zdis  24332  xrhmeo  24462  oprpiece1res1  24467  voliunlem3  25069  volsup  25073  volivth  25124  iblss2  25323  itgss  25329  coeidp  25777  dgrsub  25786  abelth  25953  reeff1olem  25958  sincosq1sgn  26008  sincosq3sgn  26010  sincosq4sgn  26011  sineq0  26033  logdivlt  26129  1cxp  26180  ecxp  26181  sinasin  26394  log2cnv  26449  efexple  26784  bposlem8  26794  lgsdir2lem2  26829  2sqb  26935  eqscut2  27307  scutun12  27311  axpaschlem  28198  axlowdimlem9  28208  axlowdimlem12  28211  axlowdimlem16  28215  axlowdimlem17  28216  sizusglecusg  28720  clwlkclwwlkf  29261  imsmetlem  29943  nmoubi  30025  nmobndi  30028  nmounbi  30029  nmlno0lem  30046  nmlnoubi  30049  isblo3i  30054  blometi  30056  blocni  30058  blocn2  30061  ipasslem2  30085  siii  30106  ubthlem1  30123  ubthlem2  30124  ubthlem3  30125  htthlem  30170  hvsubid  30279  hv2times  30314  hi01  30349  hhssabloilem  30514  pjsumi  30963  mayete3i  30981  hoaddcomi  31025  hodsi  31028  hoaddassi  31029  hocadddiri  31032  hocsubdiri  31033  hoaddridi  31039  honegsubi  31049  honegneg  31059  ho2times  31072  eigrei  31087  eigorthi  31090  nmopnegi  31218  hoddii  31242  lnophsi  31254  lnopeqi  31261  nmoptrii  31347  opsqrlem1  31393  opsqrlem6  31398  pjsdii  31408  pjddii  31409  pjscji  31423  pjssposi  31425  pjssdif2i  31427  pjtoi  31432  mdsl2bi  31576  cvmdi  31577  mdslmd3i  31585  mdslmd4i  31586  mdexchi  31588  cvati  31619  cvexchlem  31621  mdsymi  31664  dmdbr5ati  31675  cdj1i  31686  cdj3lem1  31687  xrge0infss  31973  xrge0tsmsd  32209  elrspunidl  32546  rrhre  33001  esumpinfval  33071  oms0  33296  eulerpartlems  33359  eulerpartlemgf  33378  probmeasb  33429  acycgr2v  34141  cvmliftlem5  34280  bcneg1  34706  wsuceq3  34789  fullfunfv  34919  finminlem  35203  nn0prpwlem  35207  bj-ceqsalg0  35768  bj-ceqsalgALT  35770  bj-ceqsalgvALT  35772  bj-vtoclgfALT  35940  finxpreclem4  36275  sin2h  36478  cos2h  36479  tan2h  36480  poimirlem1  36489  poimirlem2  36490  poimirlem3  36491  poimirlem4  36492  poimirlem6  36494  poimirlem7  36495  poimirlem11  36499  poimirlem12  36500  poimirlem16  36504  poimirlem17  36505  poimirlem19  36507  poimirlem20  36508  poimirlem23  36511  poimirlem30  36518  poimirlem32  36520  poimir  36521  broucube  36522  mblfinlem1  36525  mblfinlem3  36527  mblfinlem4  36528  ismblfin  36529  volsupnfl  36533  iblmulc2nc  36553  ftc1anc  36569  dvasin  36572  heiborlem3  36681  heiborlem6  36684  heiborlem8  36686  cdleme32fva  39308  2xp3dxp2ge1d  41022  isnumbasgrplem1  41843  areaquad  41965  binomcxplemnotnn0  43115  fourierdlem101  44923  fourierdlem103  44925  fourierdlem104  44926  sqwvfourb  44945  fourierswlem  44946  fouriersw  44947  m1mod0mod1  46037  sgoldbeven3prm  46451  iooii  47550  aacllem  47848