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

Theorem 3bitr4rd 221
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 191 . 2 (𝜑 → (𝜏𝜓))
4 3bitr4d.2 . 2 (𝜑 → (𝜃𝜓))
53, 4bitr4d 191 1 (𝜑 → (𝜏𝜃))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 105
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108
This theorem depends on definitions:  df-bi 117
This theorem is referenced by:  inimasn  5048  dmfco  5587  omp1eomlem  7096  ltanqg  7402  genpassl  7526  genpassu  7527  ltexprlemloc  7609  caucvgprlemcanl  7646  cauappcvgprlemladdrl  7659  caucvgprlemladdrl  7680  caucvgprprlemaddq  7710  apneg  8571  lemuldiv  8841  msq11  8862  negiso  8915  avglt2  9161  xleaddadd  9890  iooshf  9955  qtri3or  10246  sq11ap  10691  hashen  10767  fihashdom  10786  cjap  10918  sqrt11ap  11050  mingeb  11253  xrnegiso  11273  clim2c  11295  climabs0  11318  absefib  11781  efieq1re  11782  nndivides  11807  oddnn02np1  11888  oddge22np1  11889  evennn02n  11890  evennn2n  11891  halfleoddlt  11902  pc2dvds  12332  pcmpt  12344  issubm  12870  cnntr  13886  cndis  13902  cnpdis  13903  lmres  13909  txhmeo  13980  blininf  14085  cncfmet  14240
  Copyright terms: Public domain W3C validator