Theorem orbi12i 772

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 770	. 2 |- ( ( ph \/ ch ) <-> ( ph \/ th ) )
3		orbi12i.1	. . 3 |- ( ph <-> ps )
4	3	orbi1i 771	. 2 |- ( ( ph \/ th ) <-> ( ps \/ th ) )
5	2, 4	bitri 184	1 |- ( ( ph \/ ch ) <-> ( ps \/ th ) )

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

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 717

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  827  anddi  829  ifptru  998  ifpfal  999  3orbi123i  1216  3or6  1360  excxor  1423  19.33b2  1678  sbequilem  1887  sborv  1940  sbor  2008  r19.43  2701  rexun  3399  indi  3468  difindiss  3475  symdifxor  3487  unab  3488  elif  3634  dfpr2  3708  rabrsndc  3759  pwprss  3910  pwtpss  3911  unipr  3928  uniun  3933  iunun  4070  iunxun  4071  brun  4161  pwunss  4404  ordsoexmid  4684  onintexmid  4695  dcextest  4703  opthprc  4801  cnvsom  5306  ftpg  5868  tpostpos  6495  eldju  7359  djur  7360  ltexprlemloc  7922  axpre-ltwlin  8198  axpre-apti  8200  axpre-mulext  8203  axpre-suploc  8217  fz01or  10445  cbvsum  12045  fsum3  12073  cbvprod  12244  fprodseq  12269  gcdsupex  12653  gcdsupcl  12654  pythagtriplem2  12964  pythagtrip  12981