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

This theorem is referenced by:  mp3an12i  1463  ceqsalg  3454  ceqsralvOLD  3460  brelrn  5840  predeq3  6195  funpr  6474  fvpr1  7047  fvpr2  7049  tfi  7675  peano5  7714  peano5OLD  7715  wrecseq3  8107  wfr3OLD  8140  fpm  8621  0fsupp  9080  ac6  10167  alephadd  10264  axpre-sup  10856  cnegex2  11087  addid2  11088  renegcli  11212  div0  11593  divclzi  11640  divcan1zi  11641  divcan2zi  11642  divreczi  11643  divcan3zi  11644  divcan4zi  11645  divasszi  11655  divmulzi  11656  divdirzi  11657  redivclzi  11671  ltm1  11747  mulgt1  11764  recgt1i  11802  ltmul1i  11823  ltdiv1i  11824  ltmuldivi  11825  ltmul2i  11826  lemul1i  11827  lemul2i  11828  ledivp1i  11830  ltdivp1i  11831  nnge1  11931  nngt0  11934  nnrecgt0  11946  nnunb  12159  recnz  12325  ge0gtmnf  12835  x2times  12962  xrub  12975  xrge0neqmnf  13113  1mod  13551  m1expcl2  13732  1exp  13740  expubnd  13823  iexpcyc  13851  expnbnd  13875  expnlbnd  13876  faclbnd4lem1  13935  imval2  14790  cjdivi  14830  resqrex  14890  sqrtneglem  14906  absdivzi  15047  climcndslem1  15489  climcndslem2  15490  fprodge1  15633  bpoly3  15696  sinhval  15791  coshval  15792  ef01bndlem  15821  sin01gt0  15827  cos01gt0  15828  evend2  15994  divalglem5  16034  vdwlem13  16622  prmlem1  16737  prmlem2  16749  ress0  16879  frmdplusg  18408  m1expaddsub  19021  islindf4  20955  resstopn  22245  lecldbas  22278  hmphindis  22856  cnbl0  23843  xrsmopn  23881  zdis  23885  xrhmeo  24015  oprpiece1res1  24020  voliunlem3  24621  volsup  24625  volivth  24676  iblss2  24875  itgss  24881  coeidp  25329  dgrsub  25338  abelth  25505  reeff1olem  25510  sincosq1sgn  25560  sincosq3sgn  25562  sincosq4sgn  25563  sineq0  25585  logdivlt  25681  1cxp  25732  ecxp  25733  sinasin  25944  log2cnv  25999  efexple  26334  bposlem8  26344  lgsdir2lem2  26379  2sqb  26485  axpaschlem  27211  axlowdimlem9  27221  axlowdimlem12  27224  axlowdimlem16  27228  axlowdimlem17  27229  sizusglecusg  27733  clwlkclwwlkf  28273  imsmetlem  28953  nmoubi  29035  nmobndi  29038  nmounbi  29039  nmlno0lem  29056  nmlnoubi  29059  isblo3i  29064  blometi  29066  blocni  29068  blocn2  29071  ipasslem2  29095  siii  29116  ubthlem1  29133  ubthlem2  29134  ubthlem3  29135  htthlem  29180  hvsubid  29289  hv2times  29324  hi01  29359  hhssabloilem  29524  pjsumi  29973  mayete3i  29991  hoaddcomi  30035  hodsi  30038  hoaddassi  30039  hocadddiri  30042  hocsubdiri  30043  hoaddid1i  30049  honegsubi  30059  honegneg  30069  ho2times  30082  eigrei  30097  eigorthi  30100  nmopnegi  30228  hoddii  30252  lnophsi  30264  lnopeqi  30271  nmoptrii  30357  opsqrlem1  30403  opsqrlem6  30408  pjsdii  30418  pjddii  30419  pjscji  30433  pjssposi  30435  pjssdif2i  30437  pjtoi  30442  mdsl2bi  30586  cvmdi  30587  mdslmd3i  30595  mdslmd4i  30596  mdexchi  30598  cvati  30629  cvexchlem  30631  mdsymi  30674  dmdbr5ati  30685  cdj1i  30696  cdj3lem1  30697  xrge0infss  30985  xrge0tsmsd  31219  elrspunidl  31508  rrhre  31871  esumpinfval  31941  oms0  32164  eulerpartlems  32227  eulerpartlemgf  32246  probmeasb  32297  acycgr2v  33012  cvmliftlem5  33151  bcneg1  33608  ssttrcl  33701  wsuceq3  33738  eqscut2  33927  scutun12  33931  fullfunfv  34176  finminlem  34434  nn0prpwlem  34438  bj-ceqsalg0  35000  bj-ceqsalgALT  35002  bj-ceqsalgvALT  35004  bj-vtoclgfALT  35157  finxpreclem4  35492  sin2h  35694  cos2h  35695  tan2h  35696  poimirlem1  35705  poimirlem2  35706  poimirlem3  35707  poimirlem4  35708  poimirlem6  35710  poimirlem7  35711  poimirlem11  35715  poimirlem12  35716  poimirlem16  35720  poimirlem17  35721  poimirlem19  35723  poimirlem20  35724  poimirlem23  35727  poimirlem30  35734  poimirlem32  35736  poimir  35737  broucube  35738  mblfinlem1  35741  mblfinlem3  35743  mblfinlem4  35744  ismblfin  35745  volsupnfl  35749  iblmulc2nc  35769  ftc1anc  35785  dvasin  35788  heiborlem3  35898  heiborlem6  35901  heiborlem8  35903  cdleme32fva  38378  2xp3dxp2ge1d  40090  isnumbasgrplem1  40842  areaquad  40963  binomcxplemnotnn0  41863  fourierdlem101  43638  fourierdlem103  43640  fourierdlem104  43641  sqwvfourb  43660  fourierswlem  43661  fouriersw  43662  m1mod0mod1  44709  sgoldbeven3prm  45123  iooii  46099  aacllem  46391