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  7451  omniwomnimkv  7507  nninfwlporlemd  7512  pitric  7688  ltexpi  7704  ltapig  7705  ltmpig  7706  ltanqg  7767  ltmnqg  7768  enq0breq  7803  genpassl  7891  genpassu  7892  1idprl  7957  1idpru  7958  caucvgprlemcanl  8011  ltasrg  8137  prsrlt  8154  caucvgsrlemoffcau  8165  ltpsrprg  8170  map2psrprg  8172  axpre-ltadd  8253  subsub23  8531  leadd1  8758  lemul1  8922  reapmul1lem  8923  reapmul1  8924  reapadd1  8925  apsym  8935  apadd1  8937  apti  8951  apcon4bid  8953  lediv1  9200  lt2mul2div  9210  lerec  9215  ltdiv2  9218  lediv2  9222  le2msq  9232  avgle1  9548  avgle2  9549  nn01to3  10019  qapne  10041  cnref1o  10053  xleneg  10241  xsubge0  10285  xleaddadd  10291  iooneg  10392  iccneg  10393  iccshftr  10398  iccshftl  10400  iccdil  10402  icccntr  10404  fzsplit2  10457  fzaddel  10467  fzrev  10493  elfzo  10558  nelfzo  10561  fzon  10576  elfzom1b  10649  ioo0  10696  ico0  10698  ioc0  10699  flqlt  10720  negqmod0  10770  frec2uzled  10868  expeq0  11009  nn0leexp2  11150  nn0opthlem1d  11160  leisorel  11291  cjreb  11633  ltmininf  12003  minclpr  12005  xrmaxlesup  12027  xrltmininf  12038  xrminltinf  12040  tanaddaplem  12507  nndivdvds  12565  moddvds  12568  modmulconst  12592  oddm1even  12644  ltoddhalfle  12662  bitsp1  12720  dvdssq  12810  phiprmpw  13002  eulerthlemh  13011  odzdvds  13026  pc2dvds  13111  1arith  13148  issubg3  13997  eqgid  14031  resghm2b  14067  conjghm  14081  conjnmzb  14085  ablsubsub23  14131  issrgid  14287  isringid  14332  opprsubgg  14392  opprunitd  14419  crngunit  14420  unitpropdg  14457  issubrng  14509  opprsubrngg  14521  opprdrng  14622  lsslss  14720  lsspropdg  14770  rspsn  14873  znidom  14994  psrbagconf1o  15066  cnrest2  15339  cnptoprest  15342  cnptoprest2  15343  lmss  15349  lmff  15352  txlm  15382  ismet2  15457  blres  15537  xmetec  15540  bdbl  15606  metrest  15609  cnbl0  15637  cnblcld  15638  reopnap  15649  bl2ioo  15653  limcdifap  15765  efle  15879  reapef  15881  logleb  15980  logrpap0b  15981  logdivle  16000  cxplt  16024  cxple  16025  rpcxple2  16026  rpcxplt2  16027  cxplt3  16028  cxple3  16029  apcxp2  16047  logbleb  16069  logblt  16070  lgsdilem  16158  lgsne0  16169  lgsquadlem1  16208  lgsquadlem2  16209  m1lgs  16216  2lgslem1a  16219  2lgs  16235  ausgrusgrben  16421  uspgr2wlkeq  16618  isclwwlknx  16669  eupth2lem3lem6fi  16724  iooref1o  17095