Theorem mp3an12 1450

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 397  df-3an 1088

This theorem is referenced by:  mp3an12i  1464  ceqsalg  3465  ceqsralvOLD  3471  brelrn  5854  predeq3  6210  funpr  6497  fvpr1  7074  fvpr2  7076  tfi  7709  peano5  7749  peano5OLD  7750  wrecseq3  8145  wfr3OLD  8178  fpm  8672  0fsupp  9159  ssttrcl  9482  ac6  10245  alephadd  10342  axpre-sup  10934  cnegex2  11166  addid2  11167  renegcli  11291  div0  11672  divclzi  11719  divcan1zi  11720  divcan2zi  11721  divreczi  11722  divcan3zi  11723  divcan4zi  11724  divasszi  11734  divmulzi  11735  divdirzi  11736  redivclzi  11750  ltm1  11826  mulgt1  11843  recgt1i  11881  ltmul1i  11902  ltdiv1i  11903  ltmuldivi  11904  ltmul2i  11905  lemul1i  11906  lemul2i  11907  ledivp1i  11909  ltdivp1i  11910  nnge1  12010  nngt0  12013  nnrecgt0  12025  nnunb  12238  recnz  12404  ge0gtmnf  12915  x2times  13042  xrub  13055  xrge0neqmnf  13193  1mod  13632  m1expcl2  13813  1exp  13821  expubnd  13904  iexpcyc  13932  expnbnd  13956  expnlbnd  13957  faclbnd4lem1  14016  imval2  14871  cjdivi  14911  resqrex  14971  sqrtneglem  14987  absdivzi  15128  climcndslem1  15570  climcndslem2  15571  fprodge1  15714  bpoly3  15777  sinhval  15872  coshval  15873  ef01bndlem  15902  sin01gt0  15908  cos01gt0  15909  evend2  16075  divalglem5  16115  vdwlem13  16703  prmlem1  16818  prmlem2  16830  ress0  16962  frmdplusg  18502  m1expaddsub  19115  islindf4  21054  resstopn  22346  lecldbas  22379  hmphindis  22957  cnbl0  23946  xrsmopn  23984  zdis  23988  xrhmeo  24118  oprpiece1res1  24123  voliunlem3  24725  volsup  24729  volivth  24780  iblss2  24979  itgss  24985  coeidp  25433  dgrsub  25442  abelth  25609  reeff1olem  25614  sincosq1sgn  25664  sincosq3sgn  25666  sincosq4sgn  25667  sineq0  25689  logdivlt  25785  1cxp  25836  ecxp  25837  sinasin  26048  log2cnv  26103  efexple  26438  bposlem8  26448  lgsdir2lem2  26483  2sqb  26589  axpaschlem  27317  axlowdimlem9  27327  axlowdimlem12  27330  axlowdimlem16  27334  axlowdimlem17  27335  sizusglecusg  27839  clwlkclwwlkf  28381  imsmetlem  29061  nmoubi  29143  nmobndi  29146  nmounbi  29147  nmlno0lem  29164  nmlnoubi  29167  isblo3i  29172  blometi  29174  blocni  29176  blocn2  29179  ipasslem2  29203  siii  29224  ubthlem1  29241  ubthlem2  29242  ubthlem3  29243  htthlem  29288  hvsubid  29397  hv2times  29432  hi01  29467  hhssabloilem  29632  pjsumi  30081  mayete3i  30099  hoaddcomi  30143  hodsi  30146  hoaddassi  30147  hocadddiri  30150  hocsubdiri  30151  hoaddid1i  30157  honegsubi  30167  honegneg  30177  ho2times  30190  eigrei  30205  eigorthi  30208  nmopnegi  30336  hoddii  30360  lnophsi  30372  lnopeqi  30379  nmoptrii  30465  opsqrlem1  30511  opsqrlem6  30516  pjsdii  30526  pjddii  30527  pjscji  30541  pjssposi  30543  pjssdif2i  30545  pjtoi  30550  mdsl2bi  30694  cvmdi  30695  mdslmd3i  30703  mdslmd4i  30704  mdexchi  30706  cvati  30737  cvexchlem  30739  mdsymi  30782  dmdbr5ati  30793  cdj1i  30804  cdj3lem1  30805  xrge0infss  31092  xrge0tsmsd  31326  elrspunidl  31615  rrhre  31980  esumpinfval  32050  oms0  32273  eulerpartlems  32336  eulerpartlemgf  32355  probmeasb  32406  acycgr2v  33121  cvmliftlem5  33260  bcneg1  33711  wsuceq3  33820  eqscut2  34009  scutun12  34013  fullfunfv  34258  finminlem  34516  nn0prpwlem  34520  bj-ceqsalg0  35082  bj-ceqsalgALT  35084  bj-ceqsalgvALT  35086  bj-vtoclgfALT  35239  finxpreclem4  35574  sin2h  35776  cos2h  35777  tan2h  35778  poimirlem1  35787  poimirlem2  35788  poimirlem3  35789  poimirlem4  35790  poimirlem6  35792  poimirlem7  35793  poimirlem11  35797  poimirlem12  35798  poimirlem16  35802  poimirlem17  35803  poimirlem19  35805  poimirlem20  35806  poimirlem23  35809  poimirlem30  35816  poimirlem32  35818  poimir  35819  broucube  35820  mblfinlem1  35823  mblfinlem3  35825  mblfinlem4  35826  ismblfin  35827  volsupnfl  35831  iblmulc2nc  35851  ftc1anc  35867  dvasin  35870  heiborlem3  35980  heiborlem6  35983  heiborlem8  35985  cdleme32fva  38458  2xp3dxp2ge1d  40169  isnumbasgrplem1  40933  areaquad  41054  binomcxplemnotnn0  41981  fourierdlem101  43755  fourierdlem103  43757  fourierdlem104  43758  sqwvfourb  43777  fourierswlem  43778  fouriersw  43779  m1mod0mod1  44832  sgoldbeven3prm  45246  iooii  46222  aacllem  46516