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

Theorem syl5bbr 192
Description: A syllogism inference from two biconditionals. (Contributed by NM, 5-Aug-1993.)
Hypotheses
Ref Expression
syl5bbr.1 (𝜓𝜑)
syl5bbr.2 (𝜒 → (𝜓𝜃))
Assertion
Ref Expression
syl5bbr (𝜒 → (𝜑𝜃))

Proof of Theorem syl5bbr
StepHypRef Expression
1 syl5bbr.1 . . 3 (𝜓𝜑)
21bicomi 130 . 2 (𝜑𝜓)
3 syl5bbr.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 190 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
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:  3bitr3g  220  ianordc  835  19.16  1490  19.19  1599  cbvab  2207  necon1bbiidc  2312  rspc2gv  2725  elabgt  2748  sbceq1a  2838  sbcralt  2904  sbcrext  2905  sbccsbg  2948  sbccsb2g  2949  iunpw  4275  tfis  4371  xp11m  4835  ressn  4937  fnssresb  5091  fun11iun  5237  funimass4  5318  dffo4  5410  f1ompt  5413  fliftf  5539  resoprab2  5699  ralrnmpt2  5716  rexrnmpt2  5717  1stconst  5943  2ndconst  5944  dfsmo2  6006  smoiso  6021  brecop  6334  ac6sfi  6566  prarloclemn  7002  axcaucvglemres  7378  reapti  7997  indstr  9013  iccneg  9338  sqap0  9919  sqrt00  10368  prmind2  10977
  Copyright terms: Public domain W3C validator