Theorem mp3an12 1448

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

Syntax hints:   → wi 4   ∧ w3a 1084

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 400  df-3an 1086

This theorem is referenced by:  mp3an12i  1462  ceqsalg  3445  ceqsralv  3449  brelrn  5783  predeq3  6130  funpr  6391  tfi  7567  peano5  7604  wrecseq3  7962  wfr3  7985  fpm  8457  0fsupp  8888  ac6  9940  alephadd  10037  axpre-sup  10629  cnegex2  10860  addid2  10861  renegcli  10985  div0  11366  divclzi  11413  divcan1zi  11414  divcan2zi  11415  divreczi  11416  divcan3zi  11417  divcan4zi  11418  divasszi  11428  divmulzi  11429  divdirzi  11430  redivclzi  11444  ltm1  11520  mulgt1  11537  recgt1i  11575  ltmul1i  11596  ltdiv1i  11597  ltmuldivi  11598  ltmul2i  11599  lemul1i  11600  lemul2i  11601  ledivp1i  11603  ltdivp1i  11604  nnge1  11702  nngt0  11705  nnrecgt0  11717  nnunb  11930  recnz  12096  ge0gtmnf  12606  x2times  12733  xrub  12746  xrge0neqmnf  12884  1mod  13320  m1expcl2  13501  1exp  13508  expubnd  13591  iexpcyc  13619  expnbnd  13643  expnlbnd  13644  faclbnd4lem1  13703  imval2  14558  cjdivi  14598  resqrex  14658  sqrtneglem  14674  absdivzi  14815  climcndslem1  15252  climcndslem2  15253  fprodge1  15397  bpoly3  15460  sinhval  15555  coshval  15556  ef01bndlem  15585  sin01gt0  15591  cos01gt0  15592  evend2  15758  divalglem5  15798  vdwlem13  16384  prmlem1  16499  prmlem2  16511  ress0  16616  frmdplusg  18085  m1expaddsub  18693  islindf4  20603  resstopn  21886  lecldbas  21919  hmphindis  22497  cnbl0  23475  xrsmopn  23513  zdis  23517  xrhmeo  23647  oprpiece1res1  23652  voliunlem3  24252  volsup  24256  volivth  24307  iblss2  24505  itgss  24511  coeidp  24959  dgrsub  24968  abelth  25135  reeff1olem  25140  sincosq1sgn  25190  sincosq3sgn  25192  sincosq4sgn  25193  sineq0  25215  logdivlt  25311  1cxp  25362  ecxp  25363  sinasin  25574  log2cnv  25629  efexple  25964  bposlem8  25974  lgsdir2lem2  26009  2sqb  26115  axpaschlem  26833  axlowdimlem9  26843  axlowdimlem12  26846  axlowdimlem16  26850  axlowdimlem17  26851  sizusglecusg  27352  clwlkclwwlkf  27892  imsmetlem  28572  nmoubi  28654  nmobndi  28657  nmounbi  28658  nmlno0lem  28675  nmlnoubi  28678  isblo3i  28683  blometi  28685  blocni  28687  blocn2  28690  ipasslem2  28714  siii  28735  ubthlem1  28752  ubthlem2  28753  ubthlem3  28754  htthlem  28799  hvsubid  28908  hv2times  28943  hi01  28978  hhssabloilem  29143  pjsumi  29592  mayete3i  29610  hoaddcomi  29654  hodsi  29657  hoaddassi  29658  hocadddiri  29661  hocsubdiri  29662  hoaddid1i  29668  honegsubi  29678  honegneg  29688  ho2times  29701  eigrei  29716  eigorthi  29719  nmopnegi  29847  hoddii  29871  lnophsi  29883  lnopeqi  29890  nmoptrii  29976  opsqrlem1  30022  opsqrlem6  30027  pjsdii  30037  pjddii  30038  pjscji  30052  pjssposi  30054  pjssdif2i  30056  pjtoi  30061  mdsl2bi  30205  cvmdi  30206  mdslmd3i  30214  mdslmd4i  30215  mdexchi  30217  cvati  30248  cvexchlem  30250  mdsymi  30293  dmdbr5ati  30304  cdj1i  30315  cdj3lem1  30316  xrge0infss  30607  xrge0tsmsd  30843  elrspunidl  31127  rrhre  31490  esumpinfval  31560  oms0  31783  eulerpartlems  31846  eulerpartlemgf  31865  probmeasb  31916  acycgr2v  32628  cvmliftlem5  32767  bcneg1  33217  wsuceq3  33365  eqscut2  33561  scutun12  33565  fullfunfv  33798  finminlem  34056  nn0prpwlem  34060  bj-ceqsalg0  34609  bj-ceqsalgALT  34611  bj-ceqsalgvALT  34613  bj-vtoclgfALT  34756  finxpreclem4  35091  sin2h  35327  cos2h  35328  tan2h  35329  poimirlem1  35338  poimirlem2  35339  poimirlem3  35340  poimirlem4  35341  poimirlem6  35343  poimirlem7  35344  poimirlem11  35348  poimirlem12  35349  poimirlem16  35353  poimirlem17  35354  poimirlem19  35356  poimirlem20  35357  poimirlem23  35360  poimirlem30  35367  poimirlem32  35369  poimir  35370  broucube  35371  mblfinlem1  35374  mblfinlem3  35376  mblfinlem4  35377  ismblfin  35378  volsupnfl  35382  iblmulc2nc  35402  ftc1anc  35418  dvasin  35421  heiborlem3  35531  heiborlem6  35534  heiborlem8  35536  cdleme32fva  38013  2xp3dxp2ge1d  39684  isnumbasgrplem1  40418  areaquad  40539  binomcxplemnotnn0  41433  fourierdlem101  43215  fourierdlem103  43217  fourierdlem104  43218  sqwvfourb  43237  fourierswlem  43238  fouriersw  43239  m1mod0mod1  44254  sgoldbeven3prm  44668  aacllem  45720