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	|- ( 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 191	. 2 |- ( ph -> ( ps <-> ta ) )
5	1, 4	bitrd 188	1 |- ( ph -> ( th <-> ta ) )

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  8921  reapmul1lem  8922  reapmul1  8923  reapadd1  8924  apsym  8934  apadd1  8936  apti  8950  apcon4bid  8952  lediv1  9199  lt2mul2div  9209  lerec  9214  ltdiv2  9217  lediv2  9221  le2msq  9231  avgle1  9546  avgle2  9547  nn01to3  10017  qapne  10039  cnref1o  10051  xleneg  10239  xsubge0  10283  xleaddadd  10289  iooneg  10390  iccneg  10391  iccshftr  10396  iccshftl  10398  iccdil  10400  icccntr  10402  fzsplit2  10455  fzaddel  10465  fzrev  10491  elfzo  10556  nelfzo  10559  fzon  10574  elfzom1b  10647  ioo0  10694  ico0  10696  ioc0  10697  flqlt  10718  negqmod0  10768  frec2uzled  10866  expeq0  11007  nn0leexp2  11148  nn0opthlem1d  11158  leisorel  11289  cjreb  11631  ltmininf  12001  minclpr  12003  xrmaxlesup  12025  xrltmininf  12036  xrminltinf  12038  tanaddaplem  12505  nndivdvds  12563  moddvds  12566  modmulconst  12590  oddm1even  12642  ltoddhalfle  12660  bitsp1  12718  dvdssq  12808  phiprmpw  13000  eulerthlemh  13009  odzdvds  13024  pc2dvds  13109  1arith  13146  issubg3  13995  eqgid  14029  resghm2b  14065  conjghm  14079  conjnmzb  14083  ablsubsub23  14129  issrgid  14285  isringid  14330  opprsubgg  14390  opprunitd  14417  crngunit  14418  unitpropdg  14455  issubrng  14507  opprsubrngg  14519  opprdrng  14620  lsslss  14718  lsspropdg  14768  rspsn  14871  znidom  14992  psrbagconf1o  15064  cnrest2  15337  cnptoprest  15340  cnptoprest2  15341  lmss  15347  lmff  15350  txlm  15380  ismet2  15455  blres  15535  xmetec  15538  bdbl  15604  metrest  15607  cnbl0  15635  cnblcld  15636  reopnap  15647  bl2ioo  15651  limcdifap  15763  efle  15877  reapef  15879  logleb  15976  logrpap0b  15977  cxplt  16018  cxple  16019  rpcxple2  16020  rpcxplt2  16021  cxplt3  16022  cxple3  16023  apcxp2  16041  logbleb  16063  logblt  16064  lgsdilem  16146  lgsne0  16157  lgsquadlem1  16196  lgsquadlem2  16197  m1lgs  16204  2lgslem1a  16207  2lgs  16223  ausgrusgrben  16409  uspgr2wlkeq  16606  isclwwlknx  16657  eupth2lem3lem6fi  16712  iooref1o  17083