Theorem mp3an12 1453

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 1450	. 2 ⊢ ((𝜓 ∧ 𝜒) → 𝜃)
5	1, 4	mpan 690	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  mp3an12i  1467  ceqsalg  3483  brelrn  5906  predeq3  6278  funpr  6572  fvpr1  7166  fvpr2  7167  tfi  7829  peano5  7869  wrecseq3  8296  fpm  8848  0fsupp  9341  ssttrcl  9668  ac6  10433  alephadd  10530  axpre-sup  11122  cnegex2  11356  addlid  11357  renegcli  11483  div0OLD  11871  divclzi  11917  divcan1zi  11918  divcan2zi  11919  divreczi  11920  divcan3zi  11921  divcan4zi  11922  divasszi  11932  divmulzi  11933  divdirzi  11934  redivclzi  11948  ltm1  12024  mulgt1OLD  12041  recgt1i  12080  ltmul1i  12101  ltdiv1i  12102  ltmuldivi  12103  ltmul2i  12104  lemul1i  12105  lemul2i  12106  ledivp1i  12108  ltdivp1i  12109  nnge1  12214  nngt0  12217  nnrecgt0  12229  nnunb  12438  recnz  12609  eluzsubi  12826  ge0gtmnf  13132  x2times  13259  xrub  13272  xrge0neqmnf  13413  1mod  13865  m1expcl2  14050  1exp  14056  expubnd  14143  iexpcyc  14172  expnbnd  14197  expnlbnd  14198  faclbnd4lem1  14258  imval2  15117  cjdivi  15157  resqrex  15216  sqrtneglem  15232  absdivzi  15374  climcndslem1  15815  climcndslem2  15816  fprodge1  15961  bpoly3  16024  sinhval  16122  coshval  16123  ef01bndlem  16152  sin01gt0  16158  cos01gt0  16159  evend2  16327  divalglem5  16367  vdwlem13  16964  prmlem1  17078  prmlem2  17090  ress0  17213  frmdplusg  18781  m1expaddsub  19428  islindf4  21747  resstopn  23073  lecldbas  23106  hmphindis  23684  cnbl0  24661  xrsmopn  24701  zdis  24705  xrhmeo  24844  oprpiece1res1  24849  voliunlem3  25453  volsup  25457  volivth  25508  iblss2  25707  itgss  25713  coeidp  26169  dgrsub  26178  abelth  26351  reeff1olem  26356  sincosq1sgn  26407  sincosq3sgn  26409  sincosq4sgn  26410  sineq0  26433  logdivlt  26530  1cxp  26581  ecxp  26582  sinasin  26799  log2cnv  26854  efexple  27192  bposlem8  27202  lgsdir2lem2  27237  2sqb  27343  eqscut2  27718  scutun12  27722  eucliddivs  28265  pw2cut  28335  zs12bday  28343  axpaschlem  28867  axlowdimlem9  28877  axlowdimlem12  28880  axlowdimlem16  28884  axlowdimlem17  28885  sizusglecusg  29391  clwlkclwwlkf  29937  imsmetlem  30619  nmoubi  30701  nmobndi  30704  nmounbi  30705  nmlno0lem  30722  nmlnoubi  30725  isblo3i  30730  blometi  30732  blocni  30734  blocn2  30737  ipasslem2  30761  siii  30782  ubthlem1  30799  ubthlem2  30800  ubthlem3  30801  htthlem  30846  hvsubid  30955  hv2times  30990  hi01  31025  hhssabloilem  31190  pjsumi  31639  mayete3i  31657  hoaddcomi  31701  hodsi  31704  hoaddassi  31705  hocadddiri  31708  hocsubdiri  31709  hoaddridi  31715  honegsubi  31725  honegneg  31735  ho2times  31748  eigrei  31763  eigorthi  31766  nmopnegi  31894  hoddii  31918  lnophsi  31930  lnopeqi  31937  nmoptrii  32023  opsqrlem1  32069  opsqrlem6  32074  pjsdii  32084  pjddii  32085  pjscji  32099  pjssposi  32101  pjssdif2i  32103  pjtoi  32108  mdsl2bi  32252  cvmdi  32253  mdslmd3i  32261  mdslmd4i  32262  mdexchi  32264  cvati  32295  cvexchlem  32297  mdsymi  32340  dmdbr5ati  32351  cdj1i  32362  cdj3lem1  32363  xrge0infss  32683  xrge0tsmsd  33002  elrspunidl  33399  2sqr3nconstr  33771  cos9thpinconstrlem2  33780  rrhre  34011  esumpinfval  34063  oms0  34288  eulerpartlems  34351  eulerpartlemgf  34370  probmeasb  34421  acycgr2v  35137  cvmliftlem5  35276  bcneg1  35723  wsuceq3  35805  fullfunfv  35935  finminlem  36306  nn0prpwlem  36310  bj-ceqsalg0  36876  bj-ceqsalgALT  36878  bj-ceqsalgvALT  36880  bj-vtoclgfALT  37047  finxpreclem4  37382  sin2h  37604  cos2h  37605  tan2h  37606  poimirlem1  37615  poimirlem2  37616  poimirlem3  37617  poimirlem4  37618  poimirlem6  37620  poimirlem7  37621  poimirlem11  37625  poimirlem12  37626  poimirlem16  37630  poimirlem17  37631  poimirlem19  37633  poimirlem20  37634  poimirlem23  37637  poimirlem30  37644  poimirlem32  37646  poimir  37647  broucube  37648  mblfinlem1  37651  mblfinlem3  37653  mblfinlem4  37654  ismblfin  37655  volsupnfl  37659  iblmulc2nc  37679  ftc1anc  37695  dvasin  37698  heiborlem3  37807  heiborlem6  37810  heiborlem8  37812  cdleme32fva  40431  isnumbasgrplem1  43090  areaquad  43205  binomcxplemnotnn0  44345  permaxun  45001  fourierdlem101  46205  fourierdlem103  46207  fourierdlem104  46208  sqwvfourb  46227  fourierswlem  46228  fouriersw  46229  m1mod0mod1  47355  sgoldbeven3prm  47784  pgnbgreunbgrlem2lem1  48104  pgnbgreunbgrlem2lem2  48105  pgnbgreunbgrlem2lem3  48106  iooii  48906  aacllem  49790