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  792  19.16  1429  19.19  1538  cbvab  2142  necon1bbiidc  2244  elabgt  2661  sbceq1a  2750  sbcralt  2811  sbcrext  2812  sbccsbg  2855  sbccsb2g  2856  iunpw  4161  tfis  4233  xp11m  4686  ressn  4785  fnssresb  4937  fun11iun  5072  funimass4  5149  dffo4  5240  f1ompt  5245  fliftf  5364  resoprab2  5521  ralrnmpt2  5538  rexrnmpt2  5539  1stconst  5765  2ndconst  5766  dfsmo2  5824  smoiso  5839  brecop  6107  prarloclemn  6353
  Copyright terms: Public domain W3C validator