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  8532  leadd1  8759  lemul1  8923  reapmul1lem  8924  reapmul1  8925  reapadd1  8926  apsym  8936  apadd1  8938  apti  8952  apcon4bid  8954  lediv1  9201  lt2mul2div  9211  lerec  9216  ltdiv2  9219  lediv2  9223  le2msq  9233  avgle1  9550  avgle2  9551  nn01to3  10026  qapne  10048  cnref1o  10061  xleneg  10249  xsubge0  10293  xleaddadd  10299  iooneg  10400  iccneg  10401  iccshftr  10406  iccshftl  10408  iccdil  10410  icccntr  10412  fzsplit2  10465  fzaddel  10475  fzrev  10501  elfzo  10566  nelfzo  10569  fzon  10584  elfzom1b  10657  ioo0  10704  ico0  10706  ioc0  10707  flqlt  10731  negqmod0  10781  frec2uzled  10879  expeq0  11020  nn0leexp2  11162  nn0opthlem1d  11172  leisorel  11303  cjreb  11645  ltmininf  12016  minclpr  12018  xrmaxlesup  12041  xrltmininf  12052  xrminltinf  12054  tanaddaplem  12521  nndivdvds  12579  moddvds  12582  modmulconst  12606  oddm1even  12658  ltoddhalfle  12676  bitsp1  12734  dvdssq  12824  phiprmpw  13020  eulerthlemh  13029  odzdvds  13044  pc2dvds  13129  1arith  13166  issubg3  14044  eqgid  14078  resghm2b  14114  conjghm  14128  conjnmzb  14132  ablsubsub23  14178  issrgid  14334  isringid  14379  opprsubgg  14439  opprunitd  14466  crngunit  14467  unitpropdg  14504  issubrng  14556  opprsubrngg  14568  opprdrng  14669  lsslss  14767  lsspropdg  14817  rspsn  14920  znidom  15041  psrbagconf1o  15113  cnrest2  15386  cnptoprest  15389  cnptoprest2  15390  lmss  15396  lmff  15399  txlm  15429  ismet2  15504  blres  15584  xmetec  15587  bdbl  15653  metrest  15656  cnbl0  15684  cnblcld  15685  reopnap  15696  bl2ioo  15700  limcdifap  15812  efle  15926  reapef  15928  logleb  16027  logrpap0b  16028  logdivle  16047  cxplt  16071  cxple  16072  rpcxple2  16073  rpcxplt2  16074  cxplt3  16075  cxple3  16076  apcxp2  16094  logbleb  16116  logblt  16117  lgsdilem  16244  lgsne0  16255  lgsquadlem1  16294  lgsquadlem2  16295  m1lgs  16302  2lgslem1a  16305  2lgs  16321  ausgrusgrben  16507  uspgr2wlkeq  16704  isclwwlknx  16755  eupth2lem3lem6fi  16810  iooref1o  17181