Theorem mp3an12 1451

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

Syntax hints:   → wi 4   ∧ w3a 1087

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 1089

This theorem is referenced by:  mp3an12i  1465  ceqsalg  3525  ceqsralvOLD  3532  brelrn  5967  predeq3  6336  funpr  6634  fvpr1  7227  fvpr2  7229  tfi  7890  peano5  7932  peano5OLD  7933  wrecseq3  8361  wfr3OLD  8394  fpm  8933  0fsupp  9459  ssttrcl  9784  ac6  10549  alephadd  10646  axpre-sup  11238  cnegex2  11472  addlid  11473  renegcli  11597  div0OLD  11983  divclzi  12029  divcan1zi  12030  divcan2zi  12031  divreczi  12032  divcan3zi  12033  divcan4zi  12034  divasszi  12044  divmulzi  12045  divdirzi  12046  redivclzi  12060  ltm1  12136  mulgt1OLD  12153  recgt1i  12192  ltmul1i  12213  ltdiv1i  12214  ltmuldivi  12215  ltmul2i  12216  lemul1i  12217  lemul2i  12218  ledivp1i  12220  ltdivp1i  12221  nnge1  12321  nngt0  12324  nnrecgt0  12336  nnunb  12549  recnz  12718  eluzsubi  12936  ge0gtmnf  13234  x2times  13361  xrub  13374  xrge0neqmnf  13512  1mod  13954  m1expcl2  14136  1exp  14142  expubnd  14227  iexpcyc  14256  expnbnd  14281  expnlbnd  14282  faclbnd4lem1  14342  imval2  15200  cjdivi  15240  resqrex  15299  sqrtneglem  15315  absdivzi  15456  climcndslem1  15897  climcndslem2  15898  fprodge1  16043  bpoly3  16106  sinhval  16202  coshval  16203  ef01bndlem  16232  sin01gt0  16238  cos01gt0  16239  evend2  16405  divalglem5  16445  vdwlem13  17040  prmlem1  17155  prmlem2  17167  ress0  17302  frmdplusg  18889  m1expaddsub  19540  islindf4  21881  resstopn  23215  lecldbas  23248  hmphindis  23826  cnbl0  24815  xrsmopn  24853  zdis  24857  xrhmeo  24996  oprpiece1res1  25001  voliunlem3  25606  volsup  25610  volivth  25661  iblss2  25861  itgss  25867  coeidp  26323  dgrsub  26332  abelth  26503  reeff1olem  26508  sincosq1sgn  26558  sincosq3sgn  26560  sincosq4sgn  26561  sineq0  26584  logdivlt  26681  1cxp  26732  ecxp  26733  sinasin  26950  log2cnv  27005  efexple  27343  bposlem8  27353  lgsdir2lem2  27388  2sqb  27494  eqscut2  27869  scutun12  27873  cutpw2  28435  pw2bday  28436  pw2cut  28438  zs12bday  28442  axpaschlem  28973  axlowdimlem9  28983  axlowdimlem12  28986  axlowdimlem16  28990  axlowdimlem17  28991  sizusglecusg  29499  clwlkclwwlkf  30040  imsmetlem  30722  nmoubi  30804  nmobndi  30807  nmounbi  30808  nmlno0lem  30825  nmlnoubi  30828  isblo3i  30833  blometi  30835  blocni  30837  blocn2  30840  ipasslem2  30864  siii  30885  ubthlem1  30902  ubthlem2  30903  ubthlem3  30904  htthlem  30949  hvsubid  31058  hv2times  31093  hi01  31128  hhssabloilem  31293  pjsumi  31742  mayete3i  31760  hoaddcomi  31804  hodsi  31807  hoaddassi  31808  hocadddiri  31811  hocsubdiri  31812  hoaddridi  31818  honegsubi  31828  honegneg  31838  ho2times  31851  eigrei  31866  eigorthi  31869  nmopnegi  31997  hoddii  32021  lnophsi  32033  lnopeqi  32040  nmoptrii  32126  opsqrlem1  32172  opsqrlem6  32177  pjsdii  32187  pjddii  32188  pjscji  32202  pjssposi  32204  pjssdif2i  32206  pjtoi  32211  mdsl2bi  32355  cvmdi  32356  mdslmd3i  32364  mdslmd4i  32365  mdexchi  32367  cvati  32398  cvexchlem  32400  mdsymi  32443  dmdbr5ati  32454  cdj1i  32465  cdj3lem1  32466  xrge0infss  32767  xrge0tsmsd  33041  elrspunidl  33421  rrhre  33967  esumpinfval  34037  oms0  34262  eulerpartlems  34325  eulerpartlemgf  34344  probmeasb  34395  acycgr2v  35118  cvmliftlem5  35257  bcneg1  35698  wsuceq3  35781  fullfunfv  35911  finminlem  36284  nn0prpwlem  36288  bj-ceqsalg0  36854  bj-ceqsalgALT  36856  bj-ceqsalgvALT  36858  bj-vtoclgfALT  37025  finxpreclem4  37360  sin2h  37570  cos2h  37571  tan2h  37572  poimirlem1  37581  poimirlem2  37582  poimirlem3  37583  poimirlem4  37584  poimirlem6  37586  poimirlem7  37587  poimirlem11  37591  poimirlem12  37592  poimirlem16  37596  poimirlem17  37597  poimirlem19  37599  poimirlem20  37600  poimirlem23  37603  poimirlem30  37610  poimirlem32  37612  poimir  37613  broucube  37614  mblfinlem1  37617  mblfinlem3  37619  mblfinlem4  37620  ismblfin  37621  volsupnfl  37625  iblmulc2nc  37645  ftc1anc  37661  dvasin  37664  heiborlem3  37773  heiborlem6  37776  heiborlem8  37778  cdleme32fva  40394  2xp3dxp2ge1d  42198  isnumbasgrplem1  43058  areaquad  43177  binomcxplemnotnn0  44325  fourierdlem101  46128  fourierdlem103  46130  fourierdlem104  46131  sqwvfourb  46150  fourierswlem  46151  fouriersw  46152  m1mod0mod1  47243  sgoldbeven3prm  47657  iooii  48597  aacllem  48895