Theorem 3bitr4d 220

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

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 ⊢ (𝜑 → (𝜃 ↔ 𝜓))
2		3bitr4d.1	. . 3 ⊢ (𝜑 → (𝜓 ↔ 𝜒))
3		3bitr4d.3	. . 3 ⊢ (𝜑 → (𝜏 ↔ 𝜒))
4	2, 3	bitr4d 191	. 2 ⊢ (𝜑 → (𝜓 ↔ 𝜏))
5	1, 4	bitrd 188	1 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

This proof depends on syntax axioms:   → wi 4   ↔ wb 105

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This proof depends on definitions:  df-bi 117

This theorem is used by:  ifpdfbidc  998  dfbi3dc  1446  xordidc  1448  19.32dc  1731  r19.32vdc  2700  opbrop  4854  fvopab3g  5778  respreima  5836  fmptco  5874  cocan1  5993  cocan2  5994  suppimacnvfn  6486  brtposg  6525  nnmword  6791  swoer  6835  erth  6853  brecop  6899  ecopovsymg  6908  xpdom2  7129  pw2f1odclem  7134  opabfi  7247  ctssdccl  7452  omniwomnimkv  7508  nninfwlporlemd  7513  pitric  7689  ltexpi  7705  ltapig  7706  ltmpig  7707  ltanqg  7768  ltmnqg  7769  enq0breq  7804  genpassl  7892  genpassu  7893  1idprl  7958  1idpru  7959  caucvgprlemcanl  8012  ltasrg  8138  prsrlt  8155  caucvgsrlemoffcau  8166  ltpsrprg  8171  map2psrprg  8173  axpre-ltadd  8254  subsub23  8533  leadd1  8760  lemul1  8924  reapmul1lem  8925  reapmul1  8926  reapadd1  8927  apsym  8937  apadd1  8939  apti  8953  apcon4bid  8955  lediv1  9202  lt2mul2div  9212  lerec  9217  ltdiv2  9220  lediv2  9224  le2msq  9234  avgle1  9551  avgle2  9552  nn01to3  10027  qapne  10049  cnref1o  10062  xleneg  10250  xsubge0  10294  xleaddadd  10300  iooneg  10401  iccneg  10402  iccshftr  10407  iccshftl  10409  iccdil  10411  icccntr  10413  fzsplit2  10466  fzaddel  10476  fzrev  10502  elfzo  10567  nelfzo  10570  fzon  10585  elfzom1b  10658  ioo0  10705  ico0  10707  ioc0  10708  flqlt  10732  negqmod0  10782  frec2uzled  10880  expeq0  11021  nn0leexp2  11163  nn0opthlem1d  11173  leisorel  11304  cjreb  11646  ltmininf  12018  minclpr  12020  xrmaxlesup  12043  xrltmininf  12054  xrminltinf  12056  tanaddaplem  12523  nndivdvds  12581  moddvds  12584  modmulconst  12608  oddm1even  12660  ltoddhalfle  12678  bitsp1  12736  dvdssq  12826  phiprmpw  13022  eulerthlemh  13031  odzdvds  13046  pc2dvds  13131  1arith  13168  issubg3  14046  eqgid  14080  resghm2b  14116  conjghm  14130  conjnmzb  14134  ablsubsub23  14180  issrgid  14336  isringid  14381  opprsubgg  14441  opprunitd  14468  crngunit  14469  unitpropdg  14506  issubrng  14558  opprsubrngg  14570  opprdrng  14671  lsslss  14769  lsspropdg  14819  rspsn  14922  znidom  15043  psrbagconf1o  15116  cnrest2  15389  cnptoprest  15392  cnptoprest2  15393  lmss  15399  lmff  15402  txlm  15432  ismet2  15507  blres  15587  xmetec  15590  bdbl  15656  metrest  15659  cnbl0  15687  cnblcld  15688  reopnap  15699  bl2ioo  15703  limcdifap  15815  efle  15929  reapef  15931  logleb  16030  logrpap0b  16031  logdivle  16050  cxplt  16074  cxple  16075  rpcxple2  16076  rpcxplt2  16077  cxplt3  16078  cxple3  16079  apcxp2  16097  logbleb  16119  logblt  16120  lgsdilem  16268  lgsne0  16279  lgsquadlem1  16318  lgsquadlem2  16319  m1lgs  16326  2lgslem1a  16329  2lgs  16345  ausgrusgrben  16531  uspgr2wlkeq  16728  isclwwlknx  16779  eupth2lem3lem6fi  16834  iooref1o  17205