Theorem mp3an12 1478

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

Syntax hints:   → wi 4   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  mp3an12i  1492  ceqsalg  3497  brelrn  5936  predeq3  6310  funpr  6596  fvpr1  7194  fvpr2  7195  tfi  7852  peano5  7893  wrecseq3  8317  fpm  8876  0fsupp  9353  ssttrcl  9687  ac6  10467  alephadd  10565  axpre-sup  11157  cnegex2  11395  addlid  11396  renegcli  11522  divclzi  11953  divcan1zi  11954  divcan2zi  11955  divreczi  11956  divcan3zi  11957  divcan4zi  11958  divasszi  11968  divmulzi  11969  divdirzi  11970  redivclzi  11984  ltm1  12060  recgt1i  12115  ltmul1i  12136  ltdiv1i  12137  ltmuldivi  12138  ltmul2i  12139  lemul1i  12140  lemul2i  12141  ledivp1i  12143  ltdivp1i  12144  nnge1  12267  nngt0  12270  nnrecgt0  12282  nnunb  12503  recnz  12674  eluzsubi  12897  ge0gtmnf  13201  x2times  13328  xrub  13341  xrge0neqmnf  13482  1mod  13939  m1expcl2  14124  1exp  14130  expubnd  14217  iexpcyc  14246  expnbnd  14271  expnlbnd  14272  faclbnd4lem1  14332  imval2  15205  cjdivi  15245  resqrex  15304  sqrtneglem  15320  absdivzi  15462  climcndslem1  15906  climcndslem2  15907  fprodge1  16052  bpoly3  16115  sinhval  16213  coshval  16214  ef01bndlem  16243  sin01gt0  16249  cos01gt0  16250  evend2  16418  divalglem5  16458  vdwlem13  17056  prmlem1  17170  prmlem2  17183  ress0  17306  frmdplusg  18916  m1expaddsub  19571  islindf4  21971  resstopn  23326  lecldbas  23359  hmphindis  23937  cnbl0  24913  xrsmopn  24953  zdis  24957  xrhmeo  25088  oprpiece1res1  25093  voliunlem3  25694  volsup  25698  volivth  25749  iblss2  25948  itgss  25954  coeidp  26403  dgrsub  26412  abelth  26584  reeff1olem  26589  sincosq1sgn  26643  sincosq3sgn  26645  sincosq4sgn  26646  sineq0  26669  logdivlt  26766  1cxp  26817  ecxp  26818  sinasin  27034  log2cnv  27089  efexple  27425  bposlem8  27435  lgsdir2lem2  27470  2sqb  27576  eqcuts2  27959  cutsun12  27963  eucliddivs  28549  pw2cut  28633  axpaschlem  29260  axlowdimlem9  29270  axlowdimlem12  29273  axlowdimlem16  29277  axlowdimlem17  29278  sizusglecusg  29783  clwlkclwwlkf  30329  imsmetlem  31012  nmoubi  31094  nmobndi  31097  nmounbi  31098  nmlno0lem  31115  nmlnoubi  31118  isblo3i  31123  blometi  31125  blocni  31127  blocn2  31130  ipasslem2  31154  siii  31175  ubthlem1  31192  ubthlem2  31193  ubthlem3  31194  htthlem  31239  hvsubid  31348  hv2times  31383  hi01  31418  hhssabloilem  31583  pjsumi  32032  mayete3i  32050  hoaddcomi  32094  hodsi  32097  hoaddassi  32098  hocadddiri  32101  hocsubdiri  32102  hoaddridi  32108  honegsubi  32118  honegneg  32128  ho2times  32141  eigrei  32156  eigorthi  32159  nmopnegi  32287  hoddii  32311  lnophsi  32323  lnopeqi  32330  nmoptrii  32416  opsqrlem1  32462  opsqrlem6  32467  pjsdii  32477  pjddii  32478  pjscji  32492  pjssposi  32494  pjssdif2i  32496  pjtoi  32501  mdsl2bi  32645  cvmdi  32646  mdslmd3i  32654  mdslmd4i  32655  mdexchi  32657  cvati  32688  cvexchlem  32690  mdsymi  32733  dmdbr5ati  32744  cdj1i  32755  cdj3lem1  32756  xrge0infss  33075  xrge0tsmsd  33363  elrspunidl  33706  2sqr3nconstr  34141  cos9thpinconstrlem2  34150  rrhre  34381  esumpinfval  34433  oms0  34657  eulerpartlems  34720  eulerpartlemgf  34739  probmeasb  34790  acycgr2v  35600  cvmliftlem5  35739  bcneg1  36186  wsuceq3  36265  fullfunfv  36397  finminlem  36777  nn0prpwlem  36781  regsfromunir1  36999  bj-ceqsalg0  37471  bj-ceqsalgALT  37473  bj-ceqsalgvALT  37475  bj-vtoclgfALT  37643  finxpreclem4  37988  sin2h  38209  cos2h  38210  tan2h  38211  poimirlem1  38220  poimirlem2  38221  poimirlem3  38222  poimirlem4  38223  poimirlem6  38225  poimirlem7  38226  poimirlem11  38230  poimirlem12  38231  poimirlem16  38235  poimirlem17  38236  poimirlem19  38238  poimirlem20  38239  poimirlem23  38242  poimirlem30  38249  poimirlem32  38251  poimir  38252  broucube  38253  mblfinlem1  38256  mblfinlem3  38258  mblfinlem4  38259  ismblfin  38260  volsupnfl  38264  iblmulc2nc  38284  ftc1anc  38300  dvasin  38303  heiborlem3  38412  heiborlem6  38415  heiborlem8  38417  cdleme32fva  41161  isnumbasgrplem1  43780  areaquad  43895  binomcxplemnotnn0  45018  permaxun  45672  fourierdlem101  46873  fourierdlem103  46875  fourierdlem104  46876  sqwvfourb  46895  fourierswlem  46896  fouriersw  46897  m1mod0mod1  48046  sgoldbeven3prm  48497  pgnbgreunbgrlem2lem1  48828  pgnbgreunbgrlem2lem2  48829  pgnbgreunbgrlem2lem3  48830  iooii  49645  aacllem  50550