Theorem mp3an12 1473

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

Syntax hints:   → wi 4   ∧ w3a 1099

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

This theorem is referenced by:  mp3an12i  1487  ceqsalg  3490  brelrn  5919  predeq3  6292  funpr  6577  fvpr1  7176  fvpr2  7177  tfi  7833  peano5  7874  wrecseq3  8298  fpm  8857  0fsupp  9334  ssttrcl  9668  ac6  10448  alephadd  10546  axpre-sup  11138  cnegex2  11376  addlid  11377  renegcli  11503  div0OLD  11890  divclzi  11937  divcan1zi  11938  divcan2zi  11939  divreczi  11940  divcan3zi  11941  divcan4zi  11942  divasszi  11952  divmulzi  11953  divdirzi  11954  redivclzi  11968  ltm1  12044  recgt1i  12099  ltmul1i  12120  ltdiv1i  12121  ltmuldivi  12122  ltmul2i  12123  lemul1i  12124  lemul2i  12125  ledivp1i  12127  ltdivp1i  12128  nnge1  12251  nngt0  12254  nnrecgt0  12266  nnunb  12487  recnz  12658  eluzsubi  12881  ge0gtmnf  13185  x2times  13312  xrub  13325  xrge0neqmnf  13466  1mod  13923  m1expcl2  14108  1exp  14114  expubnd  14201  iexpcyc  14230  expnbnd  14255  expnlbnd  14256  faclbnd4lem1  14316  imval2  15188  cjdivi  15228  resqrex  15287  sqrtneglem  15303  absdivzi  15445  climcndslem1  15889  climcndslem2  15890  fprodge1  16035  bpoly3  16098  sinhval  16196  coshval  16197  ef01bndlem  16226  sin01gt0  16232  cos01gt0  16233  evend2  16401  divalglem5  16441  vdwlem13  17039  prmlem1  17153  prmlem2  17166  ress0  17289  frmdplusg  18898  m1expaddsub  19548  islindf4  21897  resstopn  23253  lecldbas  23286  hmphindis  23864  cnbl0  24840  xrsmopn  24880  zdis  24884  xrhmeo  25015  oprpiece1res1  25020  voliunlem3  25621  volsup  25625  volivth  25676  iblss2  25875  itgss  25881  coeidp  26330  dgrsub  26339  abelth  26511  reeff1olem  26516  sincosq1sgn  26570  sincosq3sgn  26572  sincosq4sgn  26573  sineq0  26596  logdivlt  26693  1cxp  26744  ecxp  26745  sinasin  26961  log2cnv  27016  efexple  27352  bposlem8  27362  lgsdir2lem2  27397  2sqb  27503  eqcuts2  27886  cutsun12  27890  eucliddivs  28476  pw2cut  28560  axpaschlem  29148  axlowdimlem9  29158  axlowdimlem12  29161  axlowdimlem16  29165  axlowdimlem17  29166  sizusglecusg  29671  clwlkclwwlkf  30217  imsmetlem  30900  nmoubi  30982  nmobndi  30985  nmounbi  30986  nmlno0lem  31003  nmlnoubi  31006  isblo3i  31011  blometi  31013  blocni  31015  blocn2  31018  ipasslem2  31042  siii  31063  ubthlem1  31080  ubthlem2  31081  ubthlem3  31082  htthlem  31127  hvsubid  31236  hv2times  31271  hi01  31306  hhssabloilem  31471  pjsumi  31920  mayete3i  31938  hoaddcomi  31982  hodsi  31985  hoaddassi  31986  hocadddiri  31989  hocsubdiri  31990  hoaddridi  31996  honegsubi  32006  honegneg  32016  ho2times  32029  eigrei  32044  eigorthi  32047  nmopnegi  32175  hoddii  32199  lnophsi  32211  lnopeqi  32218  nmoptrii  32304  opsqrlem1  32350  opsqrlem6  32355  pjsdii  32365  pjddii  32366  pjscji  32380  pjssposi  32382  pjssdif2i  32384  pjtoi  32389  mdsl2bi  32533  cvmdi  32534  mdslmd3i  32542  mdslmd4i  32543  mdexchi  32545  cvati  32576  cvexchlem  32578  mdsymi  32621  dmdbr5ati  32632  cdj1i  32643  cdj3lem1  32644  xrge0infss  32968  xrge0tsmsd  33259  elrspunidl  33617  2sqr3nconstr  34080  cos9thpinconstrlem2  34089  rrhre  34320  esumpinfval  34372  oms0  34596  eulerpartlems  34659  eulerpartlemgf  34678  probmeasb  34729  acycgr2v  35505  cvmliftlem5  35644  bcneg1  36091  wsuceq3  36170  fullfunfv  36302  finminlem  36683  nn0prpwlem  36687  regsfromunir1  36905  bj-ceqsalg0  37378  bj-ceqsalgALT  37380  bj-ceqsalgvALT  37382  bj-vtoclgfALT  37549  finxpreclem4  37893  sin2h  38114  cos2h  38115  tan2h  38116  poimirlem1  38125  poimirlem2  38126  poimirlem3  38127  poimirlem4  38128  poimirlem6  38130  poimirlem7  38131  poimirlem11  38135  poimirlem12  38136  poimirlem16  38140  poimirlem17  38141  poimirlem19  38143  poimirlem20  38144  poimirlem23  38147  poimirlem30  38154  poimirlem32  38156  poimir  38157  broucube  38158  mblfinlem1  38161  mblfinlem3  38163  mblfinlem4  38164  ismblfin  38165  volsupnfl  38169  iblmulc2nc  38189  ftc1anc  38205  dvasin  38208  heiborlem3  38317  heiborlem6  38320  heiborlem8  38322  cdleme32fva  41066  isnumbasgrplem1  43683  areaquad  43798  binomcxplemnotnn0  44923  permaxun  45578  fourierdlem101  46772  fourierdlem103  46774  fourierdlem104  46775  sqwvfourb  46794  fourierswlem  46795  fouriersw  46796  m1mod0mod1  47945  sgoldbeven3prm  48396  pgnbgreunbgrlem2lem1  48727  pgnbgreunbgrlem2lem2  48728  pgnbgreunbgrlem2lem3  48729  iooii  49530  aacllem  50413