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

Theorem 3bitr4d 209
Description: Deduction from transitivity of biconditional. Useful for converting conditional definitions in a formula. (Contributed by NM, 18-Oct-1995.)
Hypotheses
Ref Expression
3bitr4d.1 (φ → (ψχ))
3bitr4d.2 (φ → (θψ))
3bitr4d.3 (φ → (τχ))
Assertion
Ref Expression
3bitr4d (φ → (θτ))

Proof of Theorem 3bitr4d
StepHypRef Expression
1 3bitr4d.2 . 2 (φ → (θψ))
2 3bitr4d.1 . . 3 (φ → (ψχ))
3 3bitr4d.3 . . 3 (φ → (τχ))
42, 3bitr4d 180 . 2 (φ → (ψτ))
51, 4bitrd 177 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:  dfbi3dc  1269  xordidc  1271  19.32dc  1547  r19.32vdc  2433  r19.12sn  3406  opbrop  4342  fvopab3g  5166  respreima  5216  fmptco  5251  cocan1  5348  cocan2  5349  brtposg  5787  nnmword  5998  swoer  6041  erth  6057  brecop  6103  ecopovsymg  6112  pitric  6175  ltexpi  6191  ltapig  6192  ltmpig  6193  ltanqg  6253  ltmnqg  6254  enq0breq  6285  genpassl  6373  genpassu  6374  1idprl  6423  1idpru  6424  ltasrg  6511  axpre-ltadd  6573  subsub23  6803  leadd1  7010
  Copyright terms: Public domain W3C validator