Theorem bibi12d 312

Description: Deduction joining two equivalences to form equivalence of biconditionals. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
bibi12d	|- (ph -> ((ps <-> th) <-> (ch <-> ta)))

Proof of Theorem bibi12d

Step	Hyp	Ref	Expression
1		imbi12d.1	. . 3 |- (ph -> (ps <-> ch))
2	1	bibi1d 310	. 2 |- (ph -> ((ps <-> th) <-> (ch <-> th)))
3		imbi12d.2	. . 3 |- (ph -> (th <-> ta))
4	3	bibi2d 309	. 2 |- (ph -> ((ch <-> th) <-> (ch <-> ta)))
5	2, 4	bitrd 244	1 |- (ph -> ((ps <-> th) <-> (ch <-> ta)))

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:  bi2bian9  845  xorbi12d  1315  cleqh  2450  abbi  2464  cleqf  2514  vtoclb  2913  vtoclbg  2916  ceqsexg  2971  elabgf  2984  reu6  3026  ru  3046  sbcbig  3093  sbcnestgf  3184  unineq  3506  preq12bg  4129  eqpw1  4163  pw111  4171  eqrelk  4213  opkelimagekg  4272  sikexlem  4296  insklem  4305  eqpw1uni  4331  cbviota  4345  iota2df  4366  opelopabsb  4698  br1stg  4731  opeliunxp2  4823  fvelimab  5371  eqfnfv  5393  fsng  5434  fressnfv  5440  isorel  5490  isocnv  5492  isotr  5496  caovord  5630  trtxp  5782  oqelins4  5795  txpcofun  5804  qrpprod  5837  fnfullfunlem1  5857  clos1basesucg  5885  extd  5924  xpassen  6058  enpw1  6063  dflec3  6222  lenc  6224  tc11  6229