Theorem orbi12i 771

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

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

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 716

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  826  anddi  828  ifptru  997  ifpfal  998  3orbi123i  1215  3or6  1359  excxor  1422  19.33b2  1677  sbequilem  1886  sborv  1939  sbor  2007  r19.43  2691  rexun  3387  indi  3454  difindiss  3461  symdifxor  3473  unab  3474  elif  3617  dfpr2  3688  rabrsndc  3739  pwprss  3889  pwtpss  3890  unipr  3907  uniun  3912  iunun  4049  iunxun  4050  brun  4140  pwunss  4380  ordsoexmid  4660  onintexmid  4671  dcextest  4679  opthprc  4777  cnvsom  5280  ftpg  5838  tpostpos  6430  eldju  7267  djur  7268  ltexprlemloc  7827  axpre-ltwlin  8103  axpre-apti  8105  axpre-mulext  8108  axpre-suploc  8122  fz01or  10346  cbvsum  11938  fsum3  11966  cbvprod  12137  fprodseq  12162  gcdsupex  12546  gcdsupcl  12547  pythagtriplem2  12857  pythagtrip  12874