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

Theorem syl2an2r 562
Description: syl2anr 284 with antecedents in standard conjunction form. (Contributed by Alan Sare, 27-Aug-2016.)
Hypotheses
Ref Expression
syl2an2r.1  |-  ( ph  ->  ps )
syl2an2r.2  |-  ( (
ph  /\  ch )  ->  th )
syl2an2r.3  |-  ( ( ps  /\  th )  ->  ta )
Assertion
Ref Expression
syl2an2r  |-  ( (
ph  /\  ch )  ->  ta )

Proof of Theorem syl2an2r
StepHypRef Expression
1 syl2an2r.1 . . 3  |-  ( ph  ->  ps )
2 syl2an2r.2 . . 3  |-  ( (
ph  /\  ch )  ->  th )
3 syl2an2r.3 . . 3  |-  ( ( ps  /\  th )  ->  ta )
41, 2, 3syl2an 283 . 2  |-  ( (
ph  /\  ( ph  /\ 
ch ) )  ->  ta )
54anabss5 545 1  |-  ( (
ph  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 102
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  op1stbg  4299  mapen  6552  supelti  6687  supmaxti  6689  infminti  6712  frecuzrdgsuc  9809  hashunlem  10200  serf0  10728  fsumabs  10846  binomlem  10864  cvgratz  10913  efcllemp  10935  ef0lem  10937  tannegap  11006  divalglemnqt  11185  lcmid  11327  hashdvds  11462
  Copyright terms: Public domain W3C validator