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

Theorem 3bitr4d 219
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 190 . 2 (𝜑 → (𝜓𝜏))
51, 4bitrd 187 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:  dfbi3dc  1375  xordidc  1377  19.32dc  1657  r19.32vdc  2580  opbrop  4621  fvopab3g  5497  respreima  5551  fmptco  5589  cocan1  5691  cocan2  5692  brtposg  6154  nnmword  6417  swoer  6460  erth  6476  brecop  6522  ecopovsymg  6531  xpdom2  6728  ctssdccl  6999  omniwomnimkv  7044  pitric  7148  ltexpi  7164  ltapig  7165  ltmpig  7166  ltanqg  7227  ltmnqg  7228  enq0breq  7263  genpassl  7351  genpassu  7352  1idprl  7417  1idpru  7418  caucvgprlemcanl  7471  ltasrg  7597  prsrlt  7614  caucvgsrlemoffcau  7625  ltpsrprg  7630  map2psrprg  7632  axpre-ltadd  7713  subsub23  7986  leadd1  8211  lemul1  8374  reapmul1lem  8375  reapmul1  8376  reapadd1  8377  apsym  8387  apadd1  8389  apti  8403  apcon4bid  8405  lediv1  8646  lt2mul2div  8656  lerec  8661  ltdiv2  8664  lediv2  8668  le2msq  8678  avgle1  8979  avgle2  8980  nn01to3  9431  qapne  9453  cnref1o  9462  xleneg  9643  xsubge0  9687  xleaddadd  9693  iooneg  9794  iccneg  9795  iccshftr  9800  iccshftl  9802  iccdil  9804  icccntr  9806  fzsplit2  9854  fzaddel  9863  fzrev  9888  elfzo  9950  fzon  9967  elfzom1b  10030  ioo0  10061  ico0  10063  ioc0  10064  flqlt  10080  negqmod0  10128  frec2uzled  10226  expeq0  10348  nn0opthlem1d  10490  leisorel  10604  cjreb  10662  ltmininf  11030  minclpr  11032  xrmaxlesup  11052  xrltmininf  11063  xrminltinf  11065  tanaddaplem  11468  nndivdvds  11522  moddvds  11525  modmulconst  11548  oddm1even  11595  ltoddhalfle  11613  dvdssq  11742  phiprmpw  11921  cnrest2  12431  cnptoprest  12434  cnptoprest2  12435  lmss  12441  lmff  12444  txlm  12474  ismet2  12549  blres  12629  xmetec  12632  bdbl  12698  metrest  12701  cnbl0  12729  cnblcld  12730  reopnap  12733  bl2ioo  12737  limcdifap  12826  efle  12892  logleb  12990  logrpap0b  12991  cxplt  13030  cxple  13031  rpcxple2  13032  rpcxplt2  13033  cxplt3  13034  cxple3  13035  logbleb  13071  logblt  13072  iooref1o  13399
  Copyright terms: Public domain W3C validator