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 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  1464  ceqsalg  3514  brelrn  5955  predeq3  6326  funpr  6623  fvpr1  7211  fvpr2  7212  tfi  7873  peano5  7915  wrecseq3  8343  wfr3OLD  8376  fpm  8913  0fsupp  9427  ssttrcl  9752  ac6  10517  alephadd  10614  axpre-sup  11206  cnegex2  11440  addlid  11441  renegcli  11567  div0OLD  11953  divclzi  11999  divcan1zi  12000  divcan2zi  12001  divreczi  12002  divcan3zi  12003  divcan4zi  12004  divasszi  12014  divmulzi  12015  divdirzi  12016  redivclzi  12030  ltm1  12106  mulgt1OLD  12123  recgt1i  12162  ltmul1i  12183  ltdiv1i  12184  ltmuldivi  12185  ltmul2i  12186  lemul1i  12187  lemul2i  12188  ledivp1i  12190  ltdivp1i  12191  nnge1  12291  nngt0  12294  nnrecgt0  12306  nnunb  12519  recnz  12690  eluzsubi  12908  ge0gtmnf  13210  x2times  13337  xrub  13350  xrge0neqmnf  13488  1mod  13939  m1expcl2  14122  1exp  14128  expubnd  14213  iexpcyc  14242  expnbnd  14267  expnlbnd  14268  faclbnd4lem1  14328  imval2  15186  cjdivi  15226  resqrex  15285  sqrtneglem  15301  absdivzi  15442  climcndslem1  15881  climcndslem2  15882  fprodge1  16027  bpoly3  16090  sinhval  16186  coshval  16187  ef01bndlem  16216  sin01gt0  16222  cos01gt0  16223  evend2  16390  divalglem5  16430  vdwlem13  17026  prmlem1  17141  prmlem2  17153  ress0  17288  frmdplusg  18879  m1expaddsub  19530  islindf4  21875  resstopn  23209  lecldbas  23242  hmphindis  23820  cnbl0  24809  xrsmopn  24847  zdis  24851  xrhmeo  24990  oprpiece1res1  24995  voliunlem3  25600  volsup  25604  volivth  25655  iblss2  25855  itgss  25861  coeidp  26317  dgrsub  26326  abelth  26499  reeff1olem  26504  sincosq1sgn  26554  sincosq3sgn  26556  sincosq4sgn  26557  sineq0  26580  logdivlt  26677  1cxp  26728  ecxp  26729  sinasin  26946  log2cnv  27001  efexple  27339  bposlem8  27349  lgsdir2lem2  27384  2sqb  27490  eqscut2  27865  scutun12  27869  cutpw2  28431  pw2bday  28432  pw2cut  28434  zs12bday  28438  axpaschlem  28969  axlowdimlem9  28979  axlowdimlem12  28982  axlowdimlem16  28986  axlowdimlem17  28987  sizusglecusg  29495  clwlkclwwlkf  30036  imsmetlem  30718  nmoubi  30800  nmobndi  30803  nmounbi  30804  nmlno0lem  30821  nmlnoubi  30824  isblo3i  30829  blometi  30831  blocni  30833  blocn2  30836  ipasslem2  30860  siii  30881  ubthlem1  30898  ubthlem2  30899  ubthlem3  30900  htthlem  30945  hvsubid  31054  hv2times  31089  hi01  31124  hhssabloilem  31289  pjsumi  31738  mayete3i  31756  hoaddcomi  31800  hodsi  31803  hoaddassi  31804  hocadddiri  31807  hocsubdiri  31808  hoaddridi  31814  honegsubi  31824  honegneg  31834  ho2times  31847  eigrei  31862  eigorthi  31865  nmopnegi  31993  hoddii  32017  lnophsi  32029  lnopeqi  32036  nmoptrii  32122  opsqrlem1  32168  opsqrlem6  32173  pjsdii  32183  pjddii  32184  pjscji  32198  pjssposi  32200  pjssdif2i  32202  pjtoi  32207  mdsl2bi  32351  cvmdi  32352  mdslmd3i  32360  mdslmd4i  32361  mdexchi  32363  cvati  32394  cvexchlem  32396  mdsymi  32439  dmdbr5ati  32450  cdj1i  32461  cdj3lem1  32462  xrge0infss  32770  xrge0tsmsd  33047  elrspunidl  33435  rrhre  33983  esumpinfval  34053  oms0  34278  eulerpartlems  34341  eulerpartlemgf  34360  probmeasb  34411  acycgr2v  35134  cvmliftlem5  35273  bcneg1  35715  wsuceq3  35798  fullfunfv  35928  finminlem  36300  nn0prpwlem  36304  bj-ceqsalg0  36870  bj-ceqsalgALT  36872  bj-ceqsalgvALT  36874  bj-vtoclgfALT  37041  finxpreclem4  37376  sin2h  37596  cos2h  37597  tan2h  37598  poimirlem1  37607  poimirlem2  37608  poimirlem3  37609  poimirlem4  37610  poimirlem6  37612  poimirlem7  37613  poimirlem11  37617  poimirlem12  37618  poimirlem16  37622  poimirlem17  37623  poimirlem19  37625  poimirlem20  37626  poimirlem23  37629  poimirlem30  37636  poimirlem32  37638  poimir  37639  broucube  37640  mblfinlem1  37643  mblfinlem3  37645  mblfinlem4  37646  ismblfin  37647  volsupnfl  37651  iblmulc2nc  37671  ftc1anc  37687  dvasin  37690  heiborlem3  37799  heiborlem6  37802  heiborlem8  37804  cdleme32fva  40419  2xp3dxp2ge1d  42222  isnumbasgrplem1  43089  areaquad  43204  binomcxplemnotnn0  44351  fourierdlem101  46162  fourierdlem103  46164  fourierdlem104  46165  sqwvfourb  46184  fourierswlem  46185  fouriersw  46186  m1mod0mod1  47293  sgoldbeven3prm  47707  iooii  48713  aacllem  49031