ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2an2r GIF version

Theorem syl2an2r 595
Description: syl2anr 290 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
Hypotheses
Ref Expression
syl2an2r.1 (𝜑𝜓)
syl2an2r.2 ((𝜑𝜒) → 𝜃)
syl2an2r.3 ((𝜓𝜃) → 𝜏)
Assertion
Ref Expression
syl2an2r ((𝜑𝜒) → 𝜏)

Proof of Theorem syl2an2r
StepHypRef Expression
1 syl2an2r.1 . . 3 (𝜑𝜓)
2 syl2an2r.2 . . 3 ((𝜑𝜒) → 𝜃)
3 syl2an2r.3 . . 3 ((𝜓𝜃) → 𝜏)
41, 2, 3syl2an 289 . 2 ((𝜑 ∧ (𝜑𝜒)) → 𝜏)
54anabss5 578 1 ((𝜑𝜒) → 𝜏)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 104
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  op1stbg  4494  mapen  6864  fival  6987  supelti  7019  supmaxti  7021  infminti  7044  xnegdi  9886  frecuzrdgsuc  10432  hashunlem  10802  2zsupmax  11252  xrmin1inf  11293  serf0  11378  fsumabs  11491  binomlem  11509  cvgratz  11558  efcllemp  11684  ef0lem  11686  tannegap  11754  modm1div  11825  divalglemnqt  11943  lcmid  12098  hashdvds  12239  prmdivdiv  12255  odzcllem  12260  reumodprminv  12271  nnnn0modprm0  12273  pythagtrip  12301  pcmpt  12359  pockthg  12373  4sqlem9  12402  ennnfonelemkh  12431  ctinf  12449  nninfdclemcl  12467  nninfdclemp1  12469  setsslid  12531  imasival  12749  imasaddflemg  12759  grpinvalem  12827  issubmnd  12869  isgrpinv  12964  grpinvssd  12987  imasgrp  13019  mulgnndir  13057  subginv  13086  subginvcl  13088  ghmpreima  13166  conjnsg  13181  srgidmlem  13293  ringidmlem  13337  imasring  13375  dvdsr01  13415  unitnegcl  13441  01eq0ring  13497  issubrng2  13518  subrginv  13545  subrgunit  13547  aprsym  13561  lmodvneg1  13607  lspsn  13693  isridlrng  13759  lidl0cl  13760  rspcl  13768  rspssid  13769  rnglidlmmgm  13773  2idlcpblrng  13799  quscrng  13808  topbas  13964  tgrest  14066  txss12  14163  cnplimclemle  14534  efltlemlt  14592  coseq0q4123  14652  lgsval  14802  lgscllem  14805  neapmkvlem  15213
  Copyright terms: Public domain W3C validator