Theorem mp3an12 1481

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 1478	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 703	1 ⊢ (𝜒 → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  mp3an12i  1495  ceqsalg  3489  brelrn  5931  predeq3  6326  funpr  6618  fvpr1  7220  fvpr2  7221  tfi  7888  peano5  7929  wrecseq3  8363  fpm  8931  0fsupp  9409  ssttrcl  9743  ac6c4  10586  ac6s  10589  alephadd  10689  axpre-sup  11281  cnegex2  11519  addlid  11520  renegcli  11646  divclzi  12079  divcan1zi  12080  divcan2zi  12081  divreczi  12082  divcan3zi  12083  divcan4zi  12084  divasszi  12094  divmulzi  12095  divdirzi  12096  redivclzi  12110  ltm1  12186  recgt1i  12241  ltmul1i  12262  ltdiv1i  12263  ltmuldivi  12264  ltmul2i  12265  lemul1i  12266  lemul2i  12267  ledivp1i  12269  ltdivp1i  12270  nnge1  12393  nngt0  12396  nnrecgt0  12408  nnunb  12629  recnz  12801  eluzsubi  13024  ge0gtmnf  13329  x2times  13456  xrub  13469  xrge0neqmnf  13610  1mod  14070  m1expcl2  14255  1exp  14261  expubnd  14348  iexpcyc  14378  expnbnd  14403  expnlbnd  14404  faclbnd4lem1  14464  imval2  15347  cjdivi  15387  resqrex  15446  sqrtneglem  15462  absdivzi  15604  climcndslem1  16047  climcndslem2  16048  fprodge1  16191  bpoly3  16253  sinhval  16351  coshval  16352  ef01bndlem  16381  sin01gt0  16387  cos01gt0  16388  evend2  16556  divalglem5  16596  vdwlem13  17200  prmlem1  17314  prmlem2  17327  ress0  17450  frmdplusg  19079  m1expaddsub  19742  islindf4  22174  resstopn  23534  lecldbas  23567  hmphindis  24146  cnbl0  25122  xrsmopn  25162  zdis  25166  xrhmeo  25297  oprpiece1res1  25302  voliunlem3  25903  volsup  25907  volivth  25958  iblss2  26156  itgss  26162  coeidp  26612  dgrsub  26621  abelth  26798  reeff1olem  26803  sincosq1sgn  26857  sincosq3sgn  26859  sincosq4sgn  26860  sineq0  26882  logdivlt  26979  1cxp  27030  ecxp  27031  sinasin  27247  log2cnv  27302  efexple  27638  bposlem8  27648  lgsdir2lem2  27683  2sqb  27789  eqcuts2  28202  cutsun12  28206  eucliddivs  28792  pw2cut  28876  axpaschlem  29548  axlowdimlem9  29558  axlowdimlem12  29561  axlowdimlem16  29565  axlowdimlem17  29566  sizusglecusg  30074  clwlkclwwlkf  30629  imsmetlem  31322  nmoubi  31404  nmobndi  31407  nmounbi  31408  nmlno0lem  31425  nmlnoubi  31428  isblo3i  31433  blometi  31435  blocni  31437  blocn2  31440  ipasslem2  31464  siii  31485  ubthlem1  31502  ubthlem2  31503  ubthlem3  31504  htthlem  31549  hvsubid  31658  hv2times  31693  hi01  31728  hhssabloilem  31893  pjsumi  32342  mayete3i  32360  hoaddcomi  32404  hodsi  32407  hoaddassi  32408  hocadddiri  32411  hocsubdiri  32412  hoaddridi  32418  honegsubi  32428  honegneg  32438  ho2times  32451  eigrei  32466  eigorthi  32469  nmopnegi  32597  hoddii  32621  lnophsi  32633  lnopeqi  32640  nmoptrii  32726  opsqrlem1  32772  opsqrlem6  32777  pjsdii  32787  pjddii  32788  pjscji  32802  pjssposi  32804  pjssdif2i  32806  pjtoi  32811  mdsl2bi  32955  cvmdi  32956  mdslmd3i  32964  mdslmd4i  32965  mdexchi  32967  cvati  32998  cvexchlem  33000  mdsymi  33043  dmdbr5ati  33054  cdj1i  33065  cdj3lem1  33066  xrge0infss  33422  xrge0tsmsd  33704  elrspunidl  34048  fedgmul  34333  2sqr3nconstr  34483  cos9thpinconstrlem2  34492  rrhre  34723  esumpinfval  34775  oms0  34999  eulerpartlems  35062  eulerpartlemgf  35081  probmeasb  35132  dfscott2  35826  dfscott3  35827  maxssj0  36006  k3n0k1lt  36023  k3n0k2lt  36024  acycgr2v  36072  cvmliftlem5  36221  bcneg1  36679  wsuceq3  36757  fullfunfv  36889  finminlem  37284  nn0prpwlem  37288  regsfromunir1  37506  bj-ceqsalg0  37978  bj-ceqsalgALT  37980  bj-ceqsalgvALT  37982  bj-vtoclgfALT  38165  finxpreclem4  38509  sin2h  38725  cos2h  38726  tan2h  38727  poimirlem1  38731  poimirlem2  38732  poimirlem3  38733  poimirlem4  38734  poimirlem6  38736  poimirlem7  38737  poimirlem11  38741  poimirlem12  38742  poimirlem16  38746  poimirlem17  38747  poimirlem19  38749  poimirlem20  38750  poimirlem23  38753  poimirlem30  38760  poimirlem32  38762  poimir  38763  broucube  38764  mblfinlem1  38767  mblfinlem3  38769  mblfinlem4  38770  ismblfin  38771  volsupnfl  38775  iblmulc2nc  38795  ftc1anc  38811  dvasin  38814  heiborlem3  38939  heiborlem6  38942  heiborlem8  38944  cdleme32fva  41686  frlmnzcoordinf  43847  isnumbasgrplem1  44295  areaquad  44410  binomcxplemnotnn0  45532  permaxun  46196  fourierdlem101  47422  fourierdlem103  47424  fourierdlem104  47425  sqwvfourb  47444  fourierswlem  47445  fouriersw  47446  m1mod0mod1  48635  sgoldbeven3prm  49086  pgnbgreunbgrlem2lem1  49417  pgnbgreunbgrlem2lem2  49418  pgnbgreunbgrlem2lem3  49419  iooii  50237  aacllem  51219