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  1886  sborv  1939  sbor  2007  r19.43  2692  rexun  3389  indi  3456  difindiss  3463  symdifxor  3475  unab  3476  elif  3621  dfpr2  3692  rabrsndc  3743  pwprss  3894  pwtpss  3895  unipr  3912  uniun  3917  iunun  4054  iunxun  4055  brun  4145  pwunss  4386  ordsoexmid  4666  onintexmid  4677  dcextest  4685  opthprc  4783  cnvsom  5287  ftpg  5846  tpostpos  6473  eldju  7327  djur  7328  ltexprlemloc  7887  axpre-ltwlin  8163  axpre-apti  8165  axpre-mulext  8168  axpre-suploc  8182  fz01or  10408  cbvsum  12000  fsum3  12028  cbvprod  12199  fprodseq  12224  gcdsupex  12608  gcdsupcl  12609  pythagtriplem2  12919  pythagtrip  12936