Theorem mp3an12 1449

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

Syntax hints:   → wi 4   ∧ w3a 1085

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 395  df-3an 1087

This theorem is referenced by:  mp3an12i  1463  ceqsalg  3506  ceqsralvOLD  3513  brelrn  5940  predeq3  6303  funpr  6603  fvpr1  7192  fvpr2  7194  tfi  7844  peano5  7886  peano5OLD  7887  wrecseq3  8307  wfr3OLD  8340  fpm  8871  0fsupp  9387  ssttrcl  9712  ac6  10477  alephadd  10574  axpre-sup  11166  cnegex2  11400  addlid  11401  renegcli  11525  div0  11906  divclzi  11953  divcan1zi  11954  divcan2zi  11955  divreczi  11956  divcan3zi  11957  divcan4zi  11958  divasszi  11968  divmulzi  11969  divdirzi  11970  redivclzi  11984  ltm1  12060  mulgt1  12077  recgt1i  12115  ltmul1i  12136  ltdiv1i  12137  ltmuldivi  12138  ltmul2i  12139  lemul1i  12140  lemul2i  12141  ledivp1i  12143  ltdivp1i  12144  nnge1  12244  nngt0  12247  nnrecgt0  12259  nnunb  12472  recnz  12641  eluzsubi  12859  ge0gtmnf  13155  x2times  13282  xrub  13295  xrge0neqmnf  13433  1mod  13872  m1expcl2  14055  1exp  14061  expubnd  14146  iexpcyc  14175  expnbnd  14199  expnlbnd  14200  faclbnd4lem1  14257  imval2  15102  cjdivi  15142  resqrex  15201  sqrtneglem  15217  absdivzi  15358  climcndslem1  15799  climcndslem2  15800  fprodge1  15943  bpoly3  16006  sinhval  16101  coshval  16102  ef01bndlem  16131  sin01gt0  16137  cos01gt0  16138  evend2  16304  divalglem5  16344  vdwlem13  16930  prmlem1  17045  prmlem2  17057  ress0  17192  frmdplusg  18771  m1expaddsub  19407  islindf4  21612  resstopn  22910  lecldbas  22943  hmphindis  23521  cnbl0  24510  xrsmopn  24548  zdis  24552  xrhmeo  24691  oprpiece1res1  24696  voliunlem3  25301  volsup  25305  volivth  25356  iblss2  25555  itgss  25561  coeidp  26013  dgrsub  26022  abelth  26189  reeff1olem  26194  sincosq1sgn  26244  sincosq3sgn  26246  sincosq4sgn  26247  sineq0  26269  logdivlt  26365  1cxp  26416  ecxp  26417  sinasin  26630  log2cnv  26685  efexple  27020  bposlem8  27030  lgsdir2lem2  27065  2sqb  27171  eqscut2  27544  scutun12  27548  axpaschlem  28465  axlowdimlem9  28475  axlowdimlem12  28478  axlowdimlem16  28482  axlowdimlem17  28483  sizusglecusg  28987  clwlkclwwlkf  29528  imsmetlem  30210  nmoubi  30292  nmobndi  30295  nmounbi  30296  nmlno0lem  30313  nmlnoubi  30316  isblo3i  30321  blometi  30323  blocni  30325  blocn2  30328  ipasslem2  30352  siii  30373  ubthlem1  30390  ubthlem2  30391  ubthlem3  30392  htthlem  30437  hvsubid  30546  hv2times  30581  hi01  30616  hhssabloilem  30781  pjsumi  31230  mayete3i  31248  hoaddcomi  31292  hodsi  31295  hoaddassi  31296  hocadddiri  31299  hocsubdiri  31300  hoaddridi  31306  honegsubi  31316  honegneg  31326  ho2times  31339  eigrei  31354  eigorthi  31357  nmopnegi  31485  hoddii  31509  lnophsi  31521  lnopeqi  31528  nmoptrii  31614  opsqrlem1  31660  opsqrlem6  31665  pjsdii  31675  pjddii  31676  pjscji  31690  pjssposi  31692  pjssdif2i  31694  pjtoi  31699  mdsl2bi  31843  cvmdi  31844  mdslmd3i  31852  mdslmd4i  31853  mdexchi  31855  cvati  31886  cvexchlem  31888  mdsymi  31931  dmdbr5ati  31942  cdj1i  31953  cdj3lem1  31954  xrge0infss  32240  xrge0tsmsd  32479  elrspunidl  32820  rrhre  33299  esumpinfval  33369  oms0  33594  eulerpartlems  33657  eulerpartlemgf  33676  probmeasb  33727  acycgr2v  34439  cvmliftlem5  34578  bcneg1  35010  wsuceq3  35093  fullfunfv  35223  finminlem  35506  nn0prpwlem  35510  bj-ceqsalg0  36071  bj-ceqsalgALT  36073  bj-ceqsalgvALT  36075  bj-vtoclgfALT  36243  finxpreclem4  36578  sin2h  36781  cos2h  36782  tan2h  36783  poimirlem1  36792  poimirlem2  36793  poimirlem3  36794  poimirlem4  36795  poimirlem6  36797  poimirlem7  36798  poimirlem11  36802  poimirlem12  36803  poimirlem16  36807  poimirlem17  36808  poimirlem19  36810  poimirlem20  36811  poimirlem23  36814  poimirlem30  36821  poimirlem32  36823  poimir  36824  broucube  36825  mblfinlem1  36828  mblfinlem3  36830  mblfinlem4  36831  ismblfin  36832  volsupnfl  36836  iblmulc2nc  36856  ftc1anc  36872  dvasin  36875  heiborlem3  36984  heiborlem6  36987  heiborlem8  36989  cdleme32fva  39611  2xp3dxp2ge1d  41328  isnumbasgrplem1  42145  areaquad  42267  binomcxplemnotnn0  43417  fourierdlem101  45221  fourierdlem103  45223  fourierdlem104  45224  sqwvfourb  45243  fourierswlem  45244  fouriersw  45245  m1mod0mod1  46335  sgoldbeven3prm  46749  iooii  47637  aacllem  47935