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

Theorem syl5bbr 183
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 123 . 2 (φψ)
3 syl5bbr.2 . 2 (χ → (ψθ))
42, 3syl5bb 181 1 (χ → (φθ))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 98
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101
This theorem depends on definitions:  df-bi 110
This theorem is referenced by:  3bitr3g  211  ianordc  798  19.16  1444  19.19  1553  cbvab  2157  necon1bbiidc  2260  elabgt  2678  sbceq1a  2767  sbcralt  2828  sbcrext  2829  sbccsbg  2872  sbccsb2g  2873  iunpw  4177  tfis  4249  xp11m  4702  ressn  4801  fnssresb  4954  fun11iun  5090  funimass4  5167  dffo4  5258  f1ompt  5263  fliftf  5382  resoprab2  5540  ralrnmpt2  5557  rexrnmpt2  5558  1stconst  5784  2ndconst  5785  dfsmo2  5843  smoiso  5858  brecop  6132  prarloclemn  6482  reapti  7363  indstr  8312  iccneg  8627
  Copyright terms: Public domain W3C validator