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-1 5  ax-2 6  ax-mp 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem depends on definitions:  df-bi 116
This theorem is referenced by:  inimasn  4892  dmfco  5421  omp1eomlem  6894  ltanqg  7109  genpassl  7233  genpassu  7234  ltexprlemloc  7316  caucvgprlemcanl  7353  cauappcvgprlemladdrl  7366  caucvgprlemladdrl  7387  caucvgprprlemaddq  7417  apneg  8239  lemuldiv  8497  msq11  8518  negiso  8571  avglt2  8811  xleaddadd  9511  iooshf  9576  qtri3or  9861  sq11ap  10299  hashen  10371  fihashdom  10390  cjap  10519  sqrt11ap  10650  xrnegiso  10870  clim2c  10892  climabs0  10915  absefib  11274  efieq1re  11275  nndivides  11295  oddnn02np1  11372  oddge22np1  11373  evennn02n  11374  evennn2n  11375  halfleoddlt  11386  cnntr  12175  cndis  12191  cnpdis  12192  lmres  12198  blininf  12352  cncfmet  12492
  Copyright terms: Public domain W3C validator