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 ⊢ (𝜑 → (𝜃 ↔ 𝜏))

Syntax hints:   → wi 4   ↔ wb 105

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  ifpdfbidc  991  dfbi3dc  1439  xordidc  1441  19.32dc  1725  r19.32vdc  2680  opbrop  4798  fvopab3g  5709  respreima  5765  fmptco  5803  cocan1  5917  cocan2  5918  brtposg  6406  nnmword  6672  swoer  6716  erth  6734  brecop  6780  ecopovsymg  6789  xpdom2  6998  pw2f1odclem  7003  opabfi  7108  ctssdccl  7286  omniwomnimkv  7342  nninfwlporlemd  7347  pitric  7516  ltexpi  7532  ltapig  7533  ltmpig  7534  ltanqg  7595  ltmnqg  7596  enq0breq  7631  genpassl  7719  genpassu  7720  1idprl  7785  1idpru  7786  caucvgprlemcanl  7839  ltasrg  7965  prsrlt  7982  caucvgsrlemoffcau  7993  ltpsrprg  7998  map2psrprg  8000  axpre-ltadd  8081  subsub23  8359  leadd1  8585  lemul1  8748  reapmul1lem  8749  reapmul1  8750  reapadd1  8751  apsym  8761  apadd1  8763  apti  8777  apcon4bid  8779  lediv1  9024  lt2mul2div  9034  lerec  9039  ltdiv2  9042  lediv2  9046  le2msq  9056  avgle1  9360  avgle2  9361  nn01to3  9820  qapne  9842  cnref1o  9854  xleneg  10041  xsubge0  10085  xleaddadd  10091  iooneg  10192  iccneg  10193  iccshftr  10198  iccshftl  10200  iccdil  10202  icccntr  10204  fzsplit2  10254  fzaddel  10263  fzrev  10288  elfzo  10353  nelfzo  10356  fzon  10371  elfzom1b  10443  ioo0  10487  ico0  10489  ioc0  10490  flqlt  10511  negqmod0  10561  frec2uzled  10659  expeq0  10800  nn0leexp2  10940  nn0opthlem1d  10950  leisorel  11067  cjreb  11385  ltmininf  11754  minclpr  11756  xrmaxlesup  11778  xrltmininf  11789  xrminltinf  11791  tanaddaplem  12257  nndivdvds  12315  moddvds  12318  modmulconst  12342  oddm1even  12394  ltoddhalfle  12412  bitsp1  12470  dvdssq  12560  phiprmpw  12752  eulerthlemh  12761  odzdvds  12776  pc2dvds  12861  1arith  12898  issubg3  13737  eqgid  13771  resghm2b  13807  conjghm  13821  conjnmzb  13825  ablsubsub23  13870  issrgid  13952  isringid  13996  opprsubgg  14055  opprunitd  14082  crngunit  14083  unitpropdg  14120  issubrng  14171  opprsubrngg  14183  lsslss  14353  lsspropdg  14403  rspsn  14506  znidom  14629  cnrest2  14918  cnptoprest  14921  cnptoprest2  14922  lmss  14928  lmff  14931  txlm  14961  ismet2  15036  blres  15116  xmetec  15119  bdbl  15185  metrest  15188  cnbl0  15216  cnblcld  15217  reopnap  15228  bl2ioo  15232  limcdifap  15344  efle  15458  reapef  15460  logleb  15557  logrpap0b  15558  cxplt  15598  cxple  15599  rpcxple2  15600  rpcxplt2  15601  cxplt3  15602  cxple3  15603  apcxp2  15621  logbleb  15643  logblt  15644  lgsdilem  15714  lgsne0  15725  lgsquadlem1  15764  lgsquadlem2  15765  m1lgs  15772  2lgslem1a  15775  2lgs  15791  ausgrusgrben  15974  uspgr2wlkeq  16086  iooref1o  16432