Theorem mp3an12 1453

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

Syntax hints:   → wi 4   ∧ w3a 1086

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 1088

This theorem is referenced by:  mp3an12i  1467  ceqsalg  3472  brelrn  5881  predeq3  6252  funpr  6537  fvpr1  7126  fvpr2  7127  tfi  7783  peano5  7823  wrecseq3  8247  fpm  8799  0fsupp  9274  ssttrcl  9605  ac6  10371  alephadd  10468  axpre-sup  11060  cnegex2  11295  addlid  11296  renegcli  11422  div0OLD  11810  divclzi  11856  divcan1zi  11857  divcan2zi  11858  divreczi  11859  divcan3zi  11860  divcan4zi  11861  divasszi  11871  divmulzi  11872  divdirzi  11873  redivclzi  11887  ltm1  11963  mulgt1OLD  11980  recgt1i  12019  ltmul1i  12040  ltdiv1i  12041  ltmuldivi  12042  ltmul2i  12043  lemul1i  12044  lemul2i  12045  ledivp1i  12047  ltdivp1i  12048  nnge1  12153  nngt0  12156  nnrecgt0  12168  nnunb  12377  recnz  12548  eluzsubi  12765  ge0gtmnf  13071  x2times  13198  xrub  13211  xrge0neqmnf  13352  1mod  13807  m1expcl2  13992  1exp  13998  expubnd  14085  iexpcyc  14114  expnbnd  14139  expnlbnd  14140  faclbnd4lem1  14200  imval2  15058  cjdivi  15098  resqrex  15157  sqrtneglem  15173  absdivzi  15315  climcndslem1  15756  climcndslem2  15757  fprodge1  15902  bpoly3  15965  sinhval  16063  coshval  16064  ef01bndlem  16093  sin01gt0  16099  cos01gt0  16100  evend2  16268  divalglem5  16308  vdwlem13  16905  prmlem1  17019  prmlem2  17031  ress0  17154  frmdplusg  18762  m1expaddsub  19410  islindf4  21775  resstopn  23101  lecldbas  23134  hmphindis  23712  cnbl0  24688  xrsmopn  24728  zdis  24732  xrhmeo  24871  oprpiece1res1  24876  voliunlem3  25480  volsup  25484  volivth  25535  iblss2  25734  itgss  25740  coeidp  26196  dgrsub  26205  abelth  26378  reeff1olem  26383  sincosq1sgn  26434  sincosq3sgn  26436  sincosq4sgn  26437  sineq0  26460  logdivlt  26557  1cxp  26608  ecxp  26609  sinasin  26826  log2cnv  26881  efexple  27219  bposlem8  27229  lgsdir2lem2  27264  2sqb  27370  eqscut2  27747  scutun12  27751  eucliddivs  28301  pw2cut  28380  zs12bday  28394  axpaschlem  28918  axlowdimlem9  28928  axlowdimlem12  28931  axlowdimlem16  28935  axlowdimlem17  28936  sizusglecusg  29442  clwlkclwwlkf  29988  imsmetlem  30670  nmoubi  30752  nmobndi  30755  nmounbi  30756  nmlno0lem  30773  nmlnoubi  30776  isblo3i  30781  blometi  30783  blocni  30785  blocn2  30788  ipasslem2  30812  siii  30833  ubthlem1  30850  ubthlem2  30851  ubthlem3  30852  htthlem  30897  hvsubid  31006  hv2times  31041  hi01  31076  hhssabloilem  31241  pjsumi  31690  mayete3i  31708  hoaddcomi  31752  hodsi  31755  hoaddassi  31756  hocadddiri  31759  hocsubdiri  31760  hoaddridi  31766  honegsubi  31776  honegneg  31786  ho2times  31799  eigrei  31814  eigorthi  31817  nmopnegi  31945  hoddii  31969  lnophsi  31981  lnopeqi  31988  nmoptrii  32074  opsqrlem1  32120  opsqrlem6  32125  pjsdii  32135  pjddii  32136  pjscji  32150  pjssposi  32152  pjssdif2i  32154  pjtoi  32159  mdsl2bi  32303  cvmdi  32304  mdslmd3i  32312  mdslmd4i  32313  mdexchi  32315  cvati  32346  cvexchlem  32348  mdsymi  32391  dmdbr5ati  32402  cdj1i  32413  cdj3lem1  32414  xrge0infss  32743  xrge0tsmsd  33042  elrspunidl  33393  2sqr3nconstr  33794  cos9thpinconstrlem2  33803  rrhre  34034  esumpinfval  34086  oms0  34310  eulerpartlems  34373  eulerpartlemgf  34392  probmeasb  34443  acycgr2v  35194  cvmliftlem5  35333  bcneg1  35780  wsuceq3  35859  fullfunfv  35991  finminlem  36362  nn0prpwlem  36366  bj-ceqsalg0  36932  bj-ceqsalgALT  36934  bj-ceqsalgvALT  36936  bj-vtoclgfALT  37103  finxpreclem4  37438  sin2h  37649  cos2h  37650  tan2h  37651  poimirlem1  37660  poimirlem2  37661  poimirlem3  37662  poimirlem4  37663  poimirlem6  37665  poimirlem7  37666  poimirlem11  37670  poimirlem12  37671  poimirlem16  37675  poimirlem17  37676  poimirlem19  37678  poimirlem20  37679  poimirlem23  37682  poimirlem30  37689  poimirlem32  37691  poimir  37692  broucube  37693  mblfinlem1  37696  mblfinlem3  37698  mblfinlem4  37699  ismblfin  37700  volsupnfl  37704  iblmulc2nc  37724  ftc1anc  37740  dvasin  37743  heiborlem3  37852  heiborlem6  37855  heiborlem8  37857  cdleme32fva  40535  isnumbasgrplem1  43193  areaquad  43308  binomcxplemnotnn0  44448  permaxun  45103  fourierdlem101  46304  fourierdlem103  46306  fourierdlem104  46307  sqwvfourb  46326  fourierswlem  46327  fouriersw  46328  m1mod0mod1  47453  sgoldbeven3prm  47882  pgnbgreunbgrlem2lem1  48213  pgnbgreunbgrlem2lem2  48214  pgnbgreunbgrlem2lem3  48215  iooii  49017  aacllem  49901