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  994  dfbi3dc  1442  xordidc  1444  19.32dc  1727  r19.32vdc  2683  opbrop  4811  fvopab3g  5728  respreima  5783  fmptco  5821  cocan1  5938  cocan2  5939  suppimacnvfn  6424  brtposg  6463  nnmword  6729  swoer  6773  erth  6791  brecop  6837  ecopovsymg  6846  xpdom2  7058  pw2f1odclem  7063  opabfi  7175  ctssdccl  7353  omniwomnimkv  7409  nninfwlporlemd  7414  pitric  7584  ltexpi  7600  ltapig  7601  ltmpig  7602  ltanqg  7663  ltmnqg  7664  enq0breq  7699  genpassl  7787  genpassu  7788  1idprl  7853  1idpru  7854  caucvgprlemcanl  7907  ltasrg  8033  prsrlt  8050  caucvgsrlemoffcau  8061  ltpsrprg  8066  map2psrprg  8068  axpre-ltadd  8149  subsub23  8427  leadd1  8653  lemul1  8816  reapmul1lem  8817  reapmul1  8818  reapadd1  8819  apsym  8829  apadd1  8831  apti  8845  apcon4bid  8847  lediv1  9092  lt2mul2div  9102  lerec  9107  ltdiv2  9110  lediv2  9114  le2msq  9124  avgle1  9428  avgle2  9429  nn01to3  9894  qapne  9916  cnref1o  9928  xleneg  10115  xsubge0  10159  xleaddadd  10165  iooneg  10266  iccneg  10267  iccshftr  10272  iccshftl  10274  iccdil  10276  icccntr  10278  fzsplit2  10328  fzaddel  10337  fzrev  10362  elfzo  10427  nelfzo  10430  fzon  10445  elfzom1b  10518  ioo0  10563  ico0  10565  ioc0  10566  flqlt  10587  negqmod0  10637  frec2uzled  10735  expeq0  10876  nn0leexp2  11016  nn0opthlem1d  11026  leisorel  11145  cjreb  11487  ltmininf  11856  minclpr  11858  xrmaxlesup  11880  xrltmininf  11891  xrminltinf  11893  tanaddaplem  12360  nndivdvds  12418  moddvds  12421  modmulconst  12445  oddm1even  12497  ltoddhalfle  12515  bitsp1  12573  dvdssq  12663  phiprmpw  12855  eulerthlemh  12864  odzdvds  12879  pc2dvds  12964  1arith  13001  issubg3  13840  eqgid  13874  resghm2b  13910  conjghm  13924  conjnmzb  13928  ablsubsub23  13973  issrgid  14056  isringid  14100  opprsubgg  14159  opprunitd  14186  crngunit  14187  unitpropdg  14224  issubrng  14275  opprsubrngg  14287  lsslss  14457  lsspropdg  14507  rspsn  14610  znidom  14733  psrbagconf1o  14754  cnrest2  15027  cnptoprest  15030  cnptoprest2  15031  lmss  15037  lmff  15040  txlm  15070  ismet2  15145  blres  15225  xmetec  15228  bdbl  15294  metrest  15297  cnbl0  15325  cnblcld  15326  reopnap  15337  bl2ioo  15341  limcdifap  15453  efle  15567  reapef  15569  logleb  15666  logrpap0b  15667  cxplt  15707  cxple  15708  rpcxple2  15709  rpcxplt2  15710  cxplt3  15711  cxple3  15712  apcxp2  15730  logbleb  15752  logblt  15753  lgsdilem  15826  lgsne0  15837  lgsquadlem1  15876  lgsquadlem2  15877  m1lgs  15884  2lgslem1a  15887  2lgs  15903  ausgrusgrben  16089  uspgr2wlkeq  16286  isclwwlknx  16337  eupth2lem3lem6fi  16392  iooref1o  16746