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

Theorem syl2an2r 569
Description: syl2anr 288 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 287 . 2 ((𝜑 ∧ (𝜑𝜒)) → 𝜏)
54anabss5 552 1 ((𝜑𝜒) → 𝜏)
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  4370  mapen  6708  fival  6826  supelti  6857  supmaxti  6859  infminti  6882  xnegdi  9619  frecuzrdgsuc  10155  hashunlem  10518  2zsupmax  10965  xrmin1inf  11004  serf0  11089  fsumabs  11202  binomlem  11220  cvgratz  11269  efcllemp  11291  ef0lem  11293  tannegap  11362  divalglemnqt  11544  lcmid  11688  hashdvds  11824  ennnfonelemkh  11852  ctinf  11870  setsslid  11936  topbas  12163  tgrest  12265  txss12  12362  cnplimclemle  12733  coseq0q4123  12842
  Copyright terms: Public domain W3C validator