Theorem orbi12i 766

Description: Infer the disjunction of two equivalences. (Contributed by NM, 5-Aug-1993.)

Hypotheses

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

Assertion

Ref	Expression
orbi12i	|- ( ( ph \/ ch ) <-> ( ps \/ th ) )

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3 |- ( ch <-> th )
2	1	orbi2i 764	. 2 |- ( ( ph \/ ch ) <-> ( ph \/ th ) )
3		orbi12i.1	. . 3 |- ( ph <-> ps )
4	3	orbi1i 765	. 2 |- ( ( ph \/ th ) <-> ( ps \/ th ) )
5	2, 4	bitri 184	1 |- ( ( ph \/ ch ) <-> ( ps \/ th ) )

Syntax hints:   <-> wb 105   \/ wo 710

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 711

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  821  anddi  823  3orbi123i  1192  3or6  1336  excxor  1398  19.33b2  1653  sbequilem  1862  sborv  1915  sbor  1983  r19.43  2666  rexun  3361  indi  3428  difindiss  3435  symdifxor  3447  unab  3448  elif  3591  dfpr2  3662  rabrsndc  3711  pwprss  3860  pwtpss  3861  unipr  3878  uniun  3883  iunun  4020  iunxun  4021  brun  4111  pwunss  4348  ordsoexmid  4628  onintexmid  4639  dcextest  4647  opthprc  4744  cnvsom  5245  ftpg  5791  tpostpos  6373  eldju  7196  djur  7197  ltexprlemloc  7755  axpre-ltwlin  8031  axpre-apti  8033  axpre-mulext  8036  axpre-suploc  8050  fz01or  10268  cbvsum  11786  fsum3  11813  cbvprod  11984  fprodseq  12009  gcdsupex  12393  gcdsupcl  12394  pythagtriplem2  12704  pythagtrip  12721