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	⊢ (φ → (ψ ↔ χ))
bitrd.2	⊢ (φ → (χ ↔ θ))

Assertion

Ref	Expression
bitrd	⊢ (φ → (ψ ↔ θ))

Proof of Theorem bitrd

Step	Hyp	Ref	Expression
1		bitrd.1	. . . 4 ⊢ (φ → (ψ ↔ χ))
2	1	pm5.74i 236	. . 3 ⊢ ((φ → ψ) ↔ (φ → χ))
3		bitrd.2	. . . 4 ⊢ (φ → (χ ↔ θ))
4	3	pm5.74i 236	. . 3 ⊢ ((φ → χ) ↔ (φ → θ))
5	2, 4	bitri 240	. 2 ⊢ ((φ → ψ) ↔ (φ → θ))
6	5	pm5.74ri 237	1 ⊢ (φ → (ψ ↔ θ))

Syntax hints:   → wi 4   ↔ wb 176

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 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  2532  neleq12d  2610  raleqbi1dv  2816  rexeqbi1dv  2817  reueqd  2818  rmoeqd  2819  raleqbidv  2820  rexeqbidv  2821  raleqbidva  2822  rexeqbidva  2823  eueq3  3012  sbc19.21g  3111  sbcrext  3120  sbcabel  3124  sbcel1g  3156  sbceq1g  3157  sbcel2g  3158  sbceq2g  3159  sbccsb2g  3166  sbcco3g  3192  elin  3220  elun  3221  sseq12d  3301  psseq12d  3364  raaan  3658  raaanv  3659  sbcss  3661  elimhyp2v  3712  elimhyp4v  3714  keephyp2v  3718  ralsng  3766  rexsng  3767  ssunsn2  3866  2ralunsn  3881  csbunig  3900  otkelins2kg  4254  otkelins3kg  4255  opkelcokg  4262  opkelimagekg  4272  reiota2  4369  eqtfinrelk  4487  vfintle  4547  breq123d  4654  sbcbr12g  4687  sbcbr1g  4688  sbcbr2g  4689  csbxpg  4814  csbrng  4967  fneq12d  5178  feq12d  5217  f1osng  5324  csbfv12g  5337  eqfnfv2  5394  funimass3  5405  funconstss  5407  dffo3  5423  fressnfv  5440  f1elima  5475  isomin  5497  f1oiso  5500  ov  5596  ovg  5602  erth2  5970  elmapg  6013  elpmg  6014  ce0nnulb  6183  ce0lenc1  6240  nmembers1lem3  6271  nchoicelem8  6297