Theorem bitr4d 530

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 520	. 2 |- (ph -> (ch <-> th))
4	1, 3	bitrd 527	1 |- (ph -> (ps <-> th))

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

This theorem is referenced by:  3bitr2d 545  3bitr2rd 546  3bitr4d 549  3bitr4rd 550  bianabs 652  sbcralt 1986  sbcralgf 1988  sbcel12g 2007  sbceqdig 2008  sbcnestg 2034  csbabg 2039  reuhyp 2900  ordtri4 2979  ordsssuc 3052  brinxp 3227  opbrop 3233  dmsnop 3323  iss 3389  fnopabfv 3749  fvelimab 3756  dmfco 3764  fvco 3765  f1fv 3865  isoini 3891  caoprord3 4050  oe1m 4169  oawordri 4174  oalimcl 4184  omlimcl 4199  oeordi 4204  ecopoprsym 4300  mapxpen 4481  ranklim 4665  r1pw 4666  r1pwcl 4667  cardnn 4804  ltsopq 5055  ltapq 5056  ltmpq 5057  ltexpq2 5061  prlem936a 5133  ltsosr 5183  ltasr 5189  xrlenltt 5481  letri3t 5498  ne0gt0t 5601  ltsubadd2t 5610  lesubadd2t 5612  sublet 5617  ltsub23t 5623  ltaddpos2t 5633  ltsubpost 5634  subge02t 5658  divne0bt 5699  rec11rt 5743  lerec 5836  ltdiv2t 5843  nnle1eq1t 5901  nnltp1let 5910  supxrre1 6048  nn0le0eq0t 6074  nn0ltp1let 6082  nn0leltp1t 6083  znnnlt1t 6111  zleltp1t 6137  flbit 6192  qbtwnre 6224  elfz5t 6414  expord2t 6543  lt2sqt 6569  le2sqt 6570  sqlecant 6580  replimt 6700  abs2difabst 6848  seq1bnd 6855  cau2 6858  bccl2t 6917  dffsum 6944  fsum1ps 6964  fsumcmpndx2 6988  serz1p 6998  climshft 7049  climres 7050  climsup 7099  efcltlem1 7254  xpnnen 7449  znnen 7453  isneip 7670  cncnp2 7729  metxp 7786  elbl2 7791  blrn3 7799  cncfmet 7857  bl2ioo 7863  lmbrf 7882  lmbrf2 7883  iscau3 7890  iscau4 7892  iscau5 7893  metcld 7917  nmoreltpnf 8377  isblo2 8388  nmlnogt0 8402  phoeqi 8462  pilem1 8609  pilem3 8611  hvmulcant 8878  hiret 8899  normgt0tOLD 8932  normgt0t 8933  pjeq2t 9179  shselt 9216  ho01 9694  ho02 9695  hoeq1t 9696  hoeq2t 9697  nmopreltpnf 9736  adjeqt 9798  lnopcon 9901  lnfncon 9928  leopt 9994  leopmul2it 10006  pjnormss 10034  pjima 10042  jplem1 10133  mddmd 10173  mdslmd1lem1 10189  mdslmd1lem2 10190  superpos 10218  atnssm0 10240  dmdbr5at 10284  nndivsub 10357  ismonb1 10617

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