Theorem orbi12i 769

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

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

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 714

This theorem depends on definitions:  df-bi 117

This theorem is referenced by:  andir  824  anddi  826  ifptru  995  ifpfal  996  3orbi123i  1213  3or6  1357  excxor  1420  19.33b2  1675  sbequilem  1884  sborv  1937  sbor  2005  r19.43  2689  rexun  3384  indi  3451  difindiss  3458  symdifxor  3470  unab  3471  elif  3614  dfpr2  3685  rabrsndc  3734  pwprss  3884  pwtpss  3885  unipr  3902  uniun  3907  iunun  4044  iunxun  4045  brun  4135  pwunss  4374  ordsoexmid  4654  onintexmid  4665  dcextest  4673  opthprc  4770  cnvsom  5272  ftpg  5823  tpostpos  6410  eldju  7235  djur  7236  ltexprlemloc  7794  axpre-ltwlin  8070  axpre-apti  8072  axpre-mulext  8075  axpre-suploc  8089  fz01or  10307  cbvsum  11871  fsum3  11898  cbvprod  12069  fprodseq  12094  gcdsupex  12478  gcdsupcl  12479  pythagtriplem2  12789  pythagtrip  12806