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  1329  xordidc  1331  19.32dc  1610  r19.32vdc  2508  opbrop  4465  fvopab3g  5297  respreima  5347  fmptco  5382  cocan1  5478  cocan2  5479  brtposg  5923  nnmword  6178  swoer  6221  erth  6237  brecop  6283  ecopovsymg  6292  xpdom2  6396  pitric  6625  ltexpi  6641  ltapig  6642  ltmpig  6643  ltanqg  6704  ltmnqg  6705  enq0breq  6740  genpassl  6828  genpassu  6829  1idprl  6894  1idpru  6895  caucvgprlemcanl  6948  ltasrg  7061  prsrlt  7077  caucvgsrlemoffcau  7088  axpre-ltadd  7166  subsub23  7432  leadd1  7653  lemul1  7812  reapmul1lem  7813  reapmul1  7814  reapadd1  7815  apsym  7825  apadd1  7827  apti  7841  lediv1  8066  lt2mul2div  8076  lerec  8081  ltdiv2  8084  lediv2  8088  le2msq  8098  avgle1  8390  avgle2  8391  nn01to3  8835  qapne  8857  cnref1o  8866  xleneg  9032  iooneg  9138  iccneg  9139  iccshftr  9144  iccshftl  9146  iccdil  9148  icccntr  9150  fzsplit2  9197  fzaddel  9205  fzrev  9229  elfzo  9288  fzon  9304  elfzom1b  9367  ioo0  9398  ico0  9400  ioc0  9401  flqlt  9417  negqmod0  9465  frec2uzled  9563  expeq0  9656  nn0opthlem1d  9796  cjreb  9954  abs00  10151  ltmininf  10317  nndivdvds  10409  moddvds  10412  modmulconst  10435  oddm1even  10482  ltoddhalfle  10500  dvdssq  10627  phiprmpw  10805
  Copyright terms: Public domain W3C validator