Theorem bitr4d 531

Description: Deduction form of bitr4 176.

Hypotheses

Ref	Expression
bitr4d.1	|- (ph -> (ps <-> ch))
bitr4d.2	|- (ph -> (th <-> ch))

Assertion

Ref	Expression
bitr4d	|- (ph -> (ps <-> th))

Proof of Theorem bitr4d

Step	Hyp	Ref	Expression
1		bitr4d.1	. 2 |- (ph -> (ps <-> ch))
2		bitr4d.2	. . 3 |- (ph -> (th <-> ch))
3	2	bicomd 521	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 528	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 3   <-> wb 146

This theorem is referenced by:  3bitr2d 546  3bitr2rd 547  3bitr4d 550  3bitr4rd 551  bianabs 653  sbcralt 1990  sbcralgf 1992  sbcel12g 2011  sbceqdig 2012  sbcnestg 2038  csbabg 2043  reuhyp 2905  ordtri4 2984  ordsssuc 3057  brinxp 3232  opbrop 3238  dmsnop 3328  iss 3397  fnopabfv 3758  fvelimab 3765  dmfco 3773  fvco 3774  f1fv 3874  isoini 3900  caoprord3 4058  oe1m 4179  oawordri 4184  oalimcl 4194  omlimcl 4209  oeordi 4214  ecopoprsym 4310  mapxpen 4495  ranklim 4685  r1pw 4686  r1pwcl 4687  cardnn 4824  ltsopq 5075  ltapq 5076  ltmpq 5077  ltexpq2 5081  prlem936a 5153  ltsosr 5203  ltasr 5209  xrlenltt 5501  letri3t 5517  ne0gt0t 5619  ltsubadd2t 5628  lesubadd2t 5630  sublet 5635  ltsub23t 5641  ltaddpos2t 5652  ltsubpost 5653  subge02t 5677  divne0bt 5728  rec11rt 5779  ltdivmul2t 5870  lerec 5880  ltdiv2t 5887  nnle1eq1t 5945  nnltp1let 5955  supxrre1 6093  nn0le0eq0t 6119  nn0ltp1let 6127  nn0leltp1t 6128  znnnlt1t 6156  zleltp1t 6182  flbit 6240  flbi2t 6241  qbtwnre 6278  elioo5t 6384  ioojoint 6416  elfz5t 6474  expord2t 6604  lt2sqt 6630  le2sqt 6631  sqlecant 6641  replimt 6761  mulretOLD 6777  abs2difabst 6903  seq1bnd 6910  cau2 6913  bccl2t 6971  dffsum 6998  fsum1ps 7018  fsumcmpndx2 7042  serz1p 7052  climshft 7104  climres 7105  climsup 7155  efcltlem1 7304  xpnnen 7499  znnen 7502  isneip 7720  cncnp2 7779  metxp 7834  elbl2 7839  blrn3 7847  cncfmet 7905  bl2ioo 7911  lmbrf 7930  lmbrf2 7931  iscau3 7938  iscau4 7940  iscau5 7941  iscaunns 7944  metcld 7967  nmoreltpnf 8432  isblo2 8443  nmlnogt0 8457  phoeqi 8518  pilem1 8671  pilem3 8673  hvmulcant 8939  hiret 8960  normgt0tOLD 8993  normgt0t 8994  pjeq2t 9241  shselt 9278  ho01 9754  ho02 9755  hoeq1t 9756  hoeq2t 9757  nmopreltpnf 9796  adjeqt 9859  lnopcon 9963  lnfncon 9990  leopt 10056  leopmul2it 10068  pjnormss 10096  pjima 10104  jplem1 10195  mddmd 10236  mdslmd1lem1 10252  mdslmd1lem2 10253  superpos 10281  atnssm0 10303  dmdbr5at 10349  nndivsub 10421  ismonb1 10739  isepib1 10749

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7

This theorem depends on definitions:  df-bi 147  df-an 225

Copyright terms: Public domain