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	|- ( ph -> ( ps <-> ch ) )
3bitr4d.2	|- ( ph -> ( th <-> ps ) )
3bitr4d.3	|- ( ph -> ( ta <-> ch ) )

Assertion

Ref	Expression
3bitr4d	|- ( ph -> ( th <-> ta ) )

Proof of Theorem 3bitr4d

Step	Hyp	Ref	Expression
1		3bitr4d.2	. 2 |- ( ph -> ( th <-> ps ) )
2		3bitr4d.1	. . 3 |- ( ph -> ( ps <-> ch ) )
3		3bitr4d.3	. . 3 |- ( ph -> ( ta <-> ch ) )
4	2, 3	bitr4d 190	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 187	1 |- ( ph -> ( th <-> ta ) )

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  1387  xordidc  1389  19.32dc  1667  r19.32vdc  2614  opbrop  4682  fvopab3g  5558  respreima  5612  fmptco  5650  cocan1  5754  cocan2  5755  brtposg  6218  nnmword  6482  swoer  6525  erth  6541  brecop  6587  ecopovsymg  6596  xpdom2  6793  ctssdccl  7072  omniwomnimkv  7127  pitric  7258  ltexpi  7274  ltapig  7275  ltmpig  7276  ltanqg  7337  ltmnqg  7338  enq0breq  7373  genpassl  7461  genpassu  7462  1idprl  7527  1idpru  7528  caucvgprlemcanl  7581  ltasrg  7707  prsrlt  7724  caucvgsrlemoffcau  7735  ltpsrprg  7740  map2psrprg  7742  axpre-ltadd  7823  subsub23  8099  leadd1  8324  lemul1  8487  reapmul1lem  8488  reapmul1  8489  reapadd1  8490  apsym  8500  apadd1  8502  apti  8516  apcon4bid  8518  lediv1  8760  lt2mul2div  8770  lerec  8775  ltdiv2  8778  lediv2  8782  le2msq  8792  avgle1  9093  avgle2  9094  nn01to3  9551  qapne  9573  cnref1o  9584  xleneg  9769  xsubge0  9813  xleaddadd  9819  iooneg  9920  iccneg  9921  iccshftr  9926  iccshftl  9928  iccdil  9930  icccntr  9932  fzsplit2  9981  fzaddel  9990  fzrev  10015  elfzo  10080  fzon  10097  elfzom1b  10160  ioo0  10191  ico0  10193  ioc0  10194  flqlt  10214  negqmod0  10262  frec2uzled  10360  expeq0  10482  nn0leexp2  10620  nn0opthlem1d  10629  leisorel  10746  cjreb  10804  ltmininf  11172  minclpr  11174  xrmaxlesup  11196  xrltmininf  11207  xrminltinf  11209  tanaddaplem  11675  nndivdvds  11732  moddvds  11735  modmulconst  11759  oddm1even  11808  ltoddhalfle  11826  dvdssq  11960  phiprmpw  12150  eulerthlemh  12159  odzdvds  12173  pc2dvds  12257  1arith  12293  cnrest2  12836  cnptoprest  12839  cnptoprest2  12840  lmss  12846  lmff  12849  txlm  12879  ismet2  12954  blres  13034  xmetec  13037  bdbl  13103  metrest  13106  cnbl0  13134  cnblcld  13135  reopnap  13138  bl2ioo  13142  limcdifap  13231  efle  13297  reapef  13299  logleb  13396  logrpap0b  13397  cxplt  13436  cxple  13437  rpcxple2  13438  rpcxplt2  13439  cxplt3  13440  cxple3  13441  apcxp2  13458  logbleb  13479  logblt  13480  lgsdilem  13528  lgsne0  13539  iooref1o  13873