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

Theorem 3bitr4d 218
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 189 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 186 1 (𝜑 → (𝜃𝜏))
Colors of variables: wff set class
Syntax hints:  wi 4  wb 103
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  dfbi3dc  1331  xordidc  1333  19.32dc  1612  r19.32vdc  2512  opbrop  4487  fvopab3g  5342  respreima  5392  fmptco  5429  cocan1  5529  cocan2  5530  brtposg  5975  nnmword  6231  swoer  6274  erth  6290  brecop  6336  ecopovsymg  6345  xpdom2  6501  pitric  6827  ltexpi  6843  ltapig  6844  ltmpig  6845  ltanqg  6906  ltmnqg  6907  enq0breq  6942  genpassl  7030  genpassu  7031  1idprl  7096  1idpru  7097  caucvgprlemcanl  7150  ltasrg  7263  prsrlt  7279  caucvgsrlemoffcau  7290  axpre-ltadd  7368  subsub23  7634  leadd1  7855  lemul1  8014  reapmul1lem  8015  reapmul1  8016  reapadd1  8017  apsym  8027  apadd1  8029  apti  8043  lediv1  8268  lt2mul2div  8278  lerec  8283  ltdiv2  8286  lediv2  8290  le2msq  8300  avgle1  8592  avgle2  8593  nn01to3  9037  qapne  9059  cnref1o  9068  xleneg  9234  iooneg  9340  iccneg  9341  iccshftr  9346  iccshftl  9348  iccdil  9350  icccntr  9352  fzsplit2  9399  fzaddel  9407  fzrev  9431  elfzo  9491  fzon  9508  elfzom1b  9571  ioo0  9602  ico0  9604  ioc0  9605  flqlt  9621  negqmod0  9669  frec2uzled  9767  expeq0  9906  nn0opthlem1d  10046  leisorel  10160  cjreb  10217  abs00  10414  ltmininf  10581  nndivdvds  10727  moddvds  10730  modmulconst  10753  oddm1even  10800  ltoddhalfle  10818  dvdssq  10945  phiprmpw  11123
  Copyright terms: Public domain W3C validator