Theorem mp3an12 1448

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

Syntax hints:   → wi 4   ∧ w3a 1084

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

This theorem is referenced by:  mp3an12i  1462  ceqsalg  3476  ceqsralv  3480  brelrn  5776  predeq3  6120  funpr  6380  tfi  7548  peano5  7585  wrecseq3  7935  wfr3  7958  fpm  8422  0fsupp  8839  ac6  9891  alephadd  9988  axpre-sup  10580  cnegex2  10811  addid2  10812  renegcli  10936  div0  11317  divclzi  11364  divcan1zi  11365  divcan2zi  11366  divreczi  11367  divcan3zi  11368  divcan4zi  11369  divasszi  11379  divmulzi  11380  divdirzi  11381  redivclzi  11395  ltm1  11471  mulgt1  11488  recgt1i  11526  ltmul1i  11547  ltdiv1i  11548  ltmuldivi  11549  ltmul2i  11550  lemul1i  11551  lemul2i  11552  ledivp1i  11554  ltdivp1i  11555  nnge1  11653  nngt0  11656  nnrecgt0  11668  nnunb  11881  recnz  12045  ge0gtmnf  12553  x2times  12680  xrub  12693  xrge0neqmnf  12830  1mod  13266  m1expcl2  13447  1exp  13454  expubnd  13537  iexpcyc  13565  expnbnd  13589  expnlbnd  13590  faclbnd4lem1  13649  imval2  14502  cjdivi  14542  resqrex  14602  sqrtneglem  14618  absdivzi  14759  climcndslem1  15196  climcndslem2  15197  fprodge1  15341  bpoly3  15404  sinhval  15499  coshval  15500  ef01bndlem  15529  sin01gt0  15535  cos01gt0  15536  evend2  15698  divalglem5  15738  vdwlem13  16319  prmlem1  16433  prmlem2  16445  ress0  16550  frmdplusg  18011  m1expaddsub  18618  islindf4  20527  resstopn  21791  lecldbas  21824  hmphindis  22402  cnbl0  23379  xrsmopn  23417  zdis  23421  xrhmeo  23551  oprpiece1res1  23556  voliunlem3  24156  volsup  24160  volivth  24211  iblss2  24409  itgss  24415  coeidp  24860  dgrsub  24869  abelth  25036  reeff1olem  25041  sincosq1sgn  25091  sincosq3sgn  25093  sincosq4sgn  25094  sineq0  25116  logdivlt  25212  1cxp  25263  ecxp  25264  sinasin  25475  log2cnv  25530  efexple  25865  bposlem8  25875  lgsdir2lem2  25910  2sqb  26016  axpaschlem  26734  axlowdimlem9  26744  axlowdimlem12  26747  axlowdimlem16  26751  axlowdimlem17  26752  sizusglecusg  27253  clwlkclwwlkf  27793  imsmetlem  28473  nmoubi  28555  nmobndi  28558  nmounbi  28559  nmlno0lem  28576  nmlnoubi  28579  isblo3i  28584  blometi  28586  blocni  28588  blocn2  28591  ipasslem2  28615  siii  28636  ubthlem1  28653  ubthlem2  28654  ubthlem3  28655  htthlem  28700  hvsubid  28809  hv2times  28844  hi01  28879  hhssabloilem  29044  pjsumi  29493  mayete3i  29511  hoaddcomi  29555  hodsi  29558  hoaddassi  29559  hocadddiri  29562  hocsubdiri  29563  hoaddid1i  29569  honegsubi  29579  honegneg  29589  ho2times  29602  eigrei  29617  eigorthi  29620  nmopnegi  29748  hoddii  29772  lnophsi  29784  lnopeqi  29791  nmoptrii  29877  opsqrlem1  29923  opsqrlem6  29928  pjsdii  29938  pjddii  29939  pjscji  29953  pjssposi  29955  pjssdif2i  29957  pjtoi  29962  mdsl2bi  30106  cvmdi  30107  mdslmd3i  30115  mdslmd4i  30116  mdexchi  30118  cvati  30149  cvexchlem  30151  mdsymi  30194  dmdbr5ati  30205  cdj1i  30216  cdj3lem1  30217  xrge0infss  30510  xrge0tsmsd  30742  elrspunidl  31014  rrhre  31372  esumpinfval  31442  oms0  31665  eulerpartlems  31728  eulerpartlemgf  31747  probmeasb  31798  acycgr2v  32510  cvmliftlem5  32649  bcneg1  33081  wsuceq3  33217  scutun12  33384  fullfunfv  33521  finminlem  33779  nn0prpwlem  33783  bj-ceqsalg0  34328  bj-ceqsalgALT  34330  bj-ceqsalgvALT  34332  bj-vtoclgfALT  34476  finxpreclem4  34811  sin2h  35047  cos2h  35048  tan2h  35049  poimirlem1  35058  poimirlem2  35059  poimirlem3  35060  poimirlem4  35061  poimirlem6  35063  poimirlem7  35064  poimirlem11  35068  poimirlem12  35069  poimirlem16  35073  poimirlem17  35074  poimirlem19  35076  poimirlem20  35077  poimirlem23  35080  poimirlem30  35087  poimirlem32  35089  poimir  35090  broucube  35091  mblfinlem1  35094  mblfinlem3  35096  mblfinlem4  35097  ismblfin  35098  volsupnfl  35102  iblmulc2nc  35122  ftc1anc  35138  dvasin  35141  heiborlem3  35251  heiborlem6  35254  heiborlem8  35256  cdleme32fva  37733  2xp3dxp2ge1d  39387  isnumbasgrplem1  40045  areaquad  40166  binomcxplemnotnn0  41060  fourierdlem101  42849  fourierdlem103  42851  fourierdlem104  42852  sqwvfourb  42871  fourierswlem  42872  fouriersw  42873  m1mod0mod1  43886  sgoldbeven3prm  44301  aacllem  45329