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  4956  dmfco  5489  omp1eomlem  6979  ltanqg  7220  genpassl  7344  genpassu  7345  ltexprlemloc  7427  caucvgprlemcanl  7464  cauappcvgprlemladdrl  7477  caucvgprlemladdrl  7498  caucvgprprlemaddq  7528  apneg  8385  lemuldiv  8651  msq11  8672  negiso  8725  avglt2  8971  xleaddadd  9682  iooshf  9747  qtri3or  10032  sq11ap  10470  hashen  10542  fihashdom  10561  cjap  10690  sqrt11ap  10822  xrnegiso  11043  clim2c  11065  climabs0  11088  absefib  11488  efieq1re  11489  nndivides  11511  oddnn02np1  11588  oddge22np1  11589  evennn02n  11590  evennn2n  11591  halfleoddlt  11602  cnntr  12408  cndis  12424  cnpdis  12425  lmres  12431  txhmeo  12502  blininf  12607  cncfmet  12762
 Copyright terms: Public domain W3C validator