Theorem bitrd 244

Description: Deduction form of bitri 240. (Contributed by NM, 5-Aug-1993.) (Proof shortened by Wolf Lammen, 14-Apr-2013.)

Hypotheses

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

Assertion

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

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 |- (ph -> (ps <-> ch))
2	1	pm5.74i 236	. . 3 |- ((ph -> ps) <-> (ph -> ch))
3		bitrd.2	. . . 4 |- (ph -> (ch <-> th))
4	3	pm5.74i 236	. . 3 |- ((ph -> ch) <-> (ph -> th))
5	2, 4	bitri 240	. 2 |- ((ph -> ps) <-> (ph -> th))
6	5	pm5.74ri 237	1 |- (ph -> (ps <-> th))

Syntax hints:   -> wi 4   <-> wb 176

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

This theorem depends on definitions:  df-bi 177

This theorem is referenced by:  bitr2d  245  bitr3d  246  bitr4d  247  syl5bb  248  syl6bb  252  3bitrd  270  3bitr2d  272  3bitr3d  274  3bitr4d  276  imbi12d  311  bibi12d  312  sylan9bb  680  orbi12d  690  anbi12d  691  dedlem0a  918  ax11el  2194  eleq12d  2421  neeq12d  2531  neleq12d  2609  raleqbi1dv  2815  rexeqbi1dv  2816  reueqd  2817  rmoeqd  2818  raleqbidv  2819  rexeqbidv  2820  raleqbidva  2821  rexeqbidva  2822  eueq3  3011  sbc19.21g  3110  sbcrext  3119  sbcabel  3123  sbcel1g  3155  sbceq1g  3156  sbcel2g  3157  sbceq2g  3158  sbccsb2g  3165  sbcco3g  3191  elin  3219  elun  3220  sseq12d  3300  psseq12d  3363  raaan  3657  raaanv  3658  sbcss  3660  elimhyp2v  3711  elimhyp4v  3713  keephyp2v  3717  ralsng  3765  rexsng  3766  ssunsn2  3865  2ralunsn  3880  csbunig  3899  otkelins2kg  4253  otkelins3kg  4254  opkelcokg  4261  opkelimagekg  4271  reiota2  4368  eqtfinrelk  4486  vfintle  4546  breq123d  4653  sbcbr12g  4686  sbcbr1g  4687  sbcbr2g  4688  csbxpg  4813  csbrng  4966  fneq12d  5177  feq12d  5216  f1osng  5323  csbfv12g  5336  eqfnfv2  5393  funimass3  5404  funconstss  5406  dffo3  5422  fressnfv  5439  f1elima  5474  isomin  5496  f1oiso  5499  ov  5595  ovg  5601  erth2  5969  elmapg  6012  elpmg  6013  ce0nnulb  6182  ce0lenc1  6239  nmembers1lem3  6270  nchoicelem8  6296