Theorem mp3an12 1479

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

This proof depends on syntax axioms:   → wi 4   ∧ w3a 1102

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 401  df-3an 1104

This theorem is used by:  mp3an12i  1493  ceqsalg  3489  brelrn  5931  predeq3  6306  funpr  6592  fvpr1  7190  fvpr2  7191  tfi  7847  peano5  7888  wrecseq3  8312  fpm  8871  0fsupp  9348  ssttrcl  9682  ac6  10470  alephadd  10568  axpre-sup  11160  cnegex2  11398  addlid  11399  renegcli  11525  divclzi  11956  divcan1zi  11957  divcan2zi  11958  divreczi  11959  divcan3zi  11960  divcan4zi  11961  divasszi  11971  divmulzi  11972  divdirzi  11973  redivclzi  11987  ltm1  12063  recgt1i  12118  ltmul1i  12139  ltdiv1i  12140  ltmuldivi  12141  ltmul2i  12142  lemul1i  12143  lemul2i  12144  ledivp1i  12146  ltdivp1i  12147  nnge1  12270  nngt0  12273  nnrecgt0  12285  nnunb  12506  recnz  12677  eluzsubi  12900  ge0gtmnf  13204  x2times  13331  xrub  13344  xrge0neqmnf  13485  1mod  13943  m1expcl2  14128  1exp  14134  expubnd  14221  iexpcyc  14250  expnbnd  14275  expnlbnd  14276  faclbnd4lem1  14336  imval2  15209  cjdivi  15249  resqrex  15308  sqrtneglem  15324  absdivzi  15466  climcndslem1  15910  climcndslem2  15911  fprodge1  16056  bpoly3  16118  sinhval  16216  coshval  16217  ef01bndlem  16246  sin01gt0  16252  cos01gt0  16253  evend2  16421  divalglem5  16461  vdwlem13  17059  prmlem1  17173  prmlem2  17186  ress0  17309  frmdplusg  18919  m1expaddsub  19574  islindf4  21999  resstopn  23354  lecldbas  23387  hmphindis  23965  cnbl0  24941  xrsmopn  24981  zdis  24985  xrhmeo  25116  oprpiece1res1  25121  voliunlem3  25722  volsup  25726  volivth  25777  iblss2  25976  itgss  25982  coeidp  26431  dgrsub  26440  abelth  26615  reeff1olem  26620  sincosq1sgn  26674  sincosq3sgn  26676  sincosq4sgn  26677  sineq0  26700  logdivlt  26797  1cxp  26848  ecxp  26849  sinasin  27065  log2cnv  27120  efexple  27456  bposlem8  27466  lgsdir2lem2  27501  2sqb  27607  eqcuts2  27990  cutsun12  27994  eucliddivs  28580  pw2cut  28664  axpaschlem  29301  axlowdimlem9  29311  axlowdimlem12  29314  axlowdimlem16  29318  axlowdimlem17  29319  sizusglecusg  29824  clwlkclwwlkf  30370  imsmetlem  31053  nmoubi  31135  nmobndi  31138  nmounbi  31139  nmlno0lem  31156  nmlnoubi  31159  isblo3i  31164  blometi  31166  blocni  31168  blocn2  31171  ipasslem2  31195  siii  31216  ubthlem1  31233  ubthlem2  31234  ubthlem3  31235  htthlem  31280  hvsubid  31389  hv2times  31424  hi01  31459  hhssabloilem  31624  pjsumi  32073  mayete3i  32091  hoaddcomi  32135  hodsi  32138  hoaddassi  32139  hocadddiri  32142  hocsubdiri  32143  hoaddridi  32149  honegsubi  32159  honegneg  32169  ho2times  32182  eigrei  32197  eigorthi  32200  nmopnegi  32328  hoddii  32352  lnophsi  32364  lnopeqi  32371  nmoptrii  32457  opsqrlem1  32503  opsqrlem6  32508  pjsdii  32518  pjddii  32519  pjscji  32533  pjssposi  32535  pjssdif2i  32537  pjtoi  32542  mdsl2bi  32686  cvmdi  32687  mdslmd3i  32695  mdslmd4i  32696  mdexchi  32698  cvati  32729  cvexchlem  32731  mdsymi  32774  dmdbr5ati  32785  cdj1i  32796  cdj3lem1  32797  xrge0infss  33116  xrge0tsmsd  33402  elrspunidl  33745  2sqr3nconstr  34180  cos9thpinconstrlem2  34189  rrhre  34420  esumpinfval  34472  oms0  34696  eulerpartlems  34759  eulerpartlemgf  34778  probmeasb  34829  dfscott2  35520  dfscott3  35521  acycgr2v  35650  cvmliftlem5  35789  bcneg1  36236  wsuceq3  36315  fullfunfv  36447  finminlem  36857  nn0prpwlem  36861  regsfromunir1  37079  bj-ceqsalg0  37551  bj-ceqsalgALT  37553  bj-ceqsalgvALT  37555  bj-vtoclgfALT  37723  finxpreclem4  38068  sin2h  38289  cos2h  38290  tan2h  38291  poimirlem1  38300  poimirlem2  38301  poimirlem3  38302  poimirlem4  38303  poimirlem6  38305  poimirlem7  38306  poimirlem11  38310  poimirlem12  38311  poimirlem16  38315  poimirlem17  38316  poimirlem19  38318  poimirlem20  38319  poimirlem23  38322  poimirlem30  38329  poimirlem32  38331  poimir  38332  broucube  38333  mblfinlem1  38336  mblfinlem3  38338  mblfinlem4  38339  ismblfin  38340  volsupnfl  38344  iblmulc2nc  38364  ftc1anc  38380  dvasin  38383  heiborlem3  38492  heiborlem6  38495  heiborlem8  38497  cdleme32fva  41239  isnumbasgrplem1  43856  areaquad  43971  binomcxplemnotnn0  45094  permaxun  45748  fourierdlem101  46949  fourierdlem103  46951  fourierdlem104  46952  sqwvfourb  46971  fourierswlem  46972  fouriersw  46973  m1mod0mod1  48125  sgoldbeven3prm  48576  pgnbgreunbgrlem2lem1  48907  pgnbgreunbgrlem2lem2  48908  pgnbgreunbgrlem2lem3  48909  iooii  49724  aacllem  50649