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

Theorem syl2an2r 590
Description: syl2anr 288 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 287 . 2  |-  ( (
ph  /\  ( ph  /\ 
ch ) )  ->  ta )
54anabss5 573 1  |-  ( (
ph  /\  ch )  ->  ta )
Colors of variables: wff set class
Syntax hints:    -> wi 4    /\ wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  op1stbg  4464  mapen  6824  fival  6947  supelti  6979  supmaxti  6981  infminti  7004  xnegdi  9825  frecuzrdgsuc  10370  hashunlem  10739  2zsupmax  11189  xrmin1inf  11230  serf0  11315  fsumabs  11428  binomlem  11446  cvgratz  11495  efcllemp  11621  ef0lem  11623  tannegap  11691  modm1div  11762  divalglemnqt  11879  lcmid  12034  hashdvds  12175  prmdivdiv  12191  odzcllem  12196  reumodprminv  12207  nnnn0modprm0  12209  pythagtrip  12237  pcmpt  12295  pockthg  12309  4sqlem9  12338  ennnfonelemkh  12367  ctinf  12385  nninfdclemp1  12405  setsslid  12466  grprinvlem  12639  isgrpinv  12756  topbas  12861  tgrest  12963  txss12  13060  cnplimclemle  13431  efltlemlt  13489  coseq0q4123  13549  lgsval  13699  lgscllem  13702  neapmkvlem  14098
  Copyright terms: Public domain W3C validator