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

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

Proof of Theorem bitr3id
StepHypRef Expression
1 bitr3id.1 . . 3 (𝜓𝜑)
21bicomi 131 . 2 (𝜑𝜓)
3 bitr3id.2 . 2 (𝜒 → (𝜓𝜃))
42, 3syl5bb 191 1 (𝜒 → (𝜑𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 104
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:  3bitr3g  221  ianordc  884  19.16  1534  19.19  1644  cbvab  2263  necon1bbiidc  2369  rspc2gv  2801  elabgt  2825  sbceq1a  2918  sbcralt  2985  sbcrext  2986  sbccsbg  3031  sbccsb2g  3032  iunpw  4401  tfis  4497  xp11m  4977  ressn  5079  fnssresb  5235  fun11iun  5388  funimass4  5472  dffo4  5568  f1ompt  5571  fliftf  5700  resoprab2  5868  ralrnmpo  5885  rexrnmpo  5886  1stconst  6118  2ndconst  6119  dfsmo2  6184  smoiso  6199  brecop  6519  ixpsnf1o  6630  ac6sfi  6792  ismkvnex  7029  prarloclemn  7319  axcaucvglemres  7719  reapti  8353  indstr  9400  iccneg  9784  sqap0  10371  sqrt00  10824  minclpr  11020  absefib  11488  efieq1re  11489  prmind2  11812  sincosq3sgn  12931  sincosq4sgn  12932  pw1nct  13282
  Copyright terms: Public domain W3C validator