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

Theorem 3bitr4rd 220
Description: Deduction from transitivity of biconditional. (Contributed by NM, 4-Aug-2006.)
Hypotheses
Ref Expression
3bitr4d.1 (𝜑 → (𝜓𝜒))
3bitr4d.2 (𝜑 → (𝜃𝜓))
3bitr4d.3 (𝜑 → (𝜏𝜒))
Assertion
Ref Expression
3bitr4rd (𝜑 → (𝜏𝜃))

Proof of Theorem 3bitr4rd
StepHypRef Expression
1 3bitr4d.3 . . 3 (𝜑 → (𝜏𝜒))
2 3bitr4d.1 . . 3 (𝜑 → (𝜓𝜒))
31, 2bitr4d 190 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 190 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:  inimasn  5028  dmfco  5564  omp1eomlem  7071  ltanqg  7362  genpassl  7486  genpassu  7487  ltexprlemloc  7569  caucvgprlemcanl  7606  cauappcvgprlemladdrl  7619  caucvgprlemladdrl  7640  caucvgprprlemaddq  7670  apneg  8530  lemuldiv  8797  msq11  8818  negiso  8871  avglt2  9117  xleaddadd  9844  iooshf  9909  qtri3or  10199  sq11ap  10643  hashen  10718  fihashdom  10738  cjap  10870  sqrt11ap  11002  mingeb  11205  xrnegiso  11225  clim2c  11247  climabs0  11270  absefib  11733  efieq1re  11734  nndivides  11759  oddnn02np1  11839  oddge22np1  11840  evennn02n  11841  evennn2n  11842  halfleoddlt  11853  pc2dvds  12283  pcmpt  12295  issubm  12695  cnntr  13019  cndis  13035  cnpdis  13036  lmres  13042  txhmeo  13113  blininf  13218  cncfmet  13373
  Copyright terms: Public domain W3C validator