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  5837  tpostpos  6429  eldju  7266  djur  7267  ltexprlemloc  7826  axpre-ltwlin  8102  axpre-apti  8104  axpre-mulext  8107  axpre-suploc  8121  fz01or  10345  cbvsum  11920  fsum3  11947  cbvprod  12118  fprodseq  12143  gcdsupex  12527  gcdsupcl  12528  pythagtriplem2  12838  pythagtrip  12855