ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  syl2an2r GIF 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 (𝜑𝜓)
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 283 . 2 ((𝜑 ∧ (𝜑𝜒)) → 𝜏)
54anabss5 545 1 ((𝜑𝜒) → 𝜏)
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  4301  mapen  6560  supelti  6695  supmaxti  6697  infminti  6720  frecuzrdgsuc  9817  hashunlem  10208  2zsupmax  10653  serf0  10737  fsumabs  10855  binomlem  10873  cvgratz  10922  efcllemp  10944  ef0lem  10946  tannegap  11015  divalglemnqt  11194  lcmid  11336  hashdvds  11471  setsidn  11539
  Copyright terms: Public domain W3C validator