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  1652  sbequilem  1861  sborv  1914  sbor  1982  r19.43  2664  rexun  3353  indi  3420  difindiss  3427  symdifxor  3439  unab  3440  dfpr2  3652  rabrsndc  3701  pwprss  3846  pwtpss  3847  unipr  3864  uniun  3869  iunun  4006  iunxun  4007  brun  4096  pwunss  4331  ordsoexmid  4611  onintexmid  4622  dcextest  4630  opthprc  4727  cnvsom  5227  ftpg  5770  tpostpos  6352  eldju  7172  djur  7173  ltexprlemloc  7722  axpre-ltwlin  7998  axpre-apti  8000  axpre-mulext  8003  axpre-suploc  8017  fz01or  10235  cbvsum  11704  fsum3  11731  cbvprod  11902  fprodseq  11927  gcdsupex  12311  gcdsupcl  12312  pythagtriplem2  12622  pythagtrip  12639