Theorem orbi12i 776

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

This proof depends on syntax axioms:   <-> wb 105   \/ wo 720

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108  ax-io 721

This proof depends on definitions:  df-bi 117

This theorem is used by:  andir  831  anddi  833  ifptru  1002  ifpfal  1003  3orbi123i  1220  3or6  1364  excxor  1427  19.33b2  1682  sbequilem  1891  sborv  1945  sbor  2014  r19.43  2709  rexun  3409  indi  3478  difindiss  3485  symdifxor  3497  unab  3498  elif  3652  dfpr2  3728  rabrsndc  3779  pwprss  3931  pwtpss  3932  unipr  3949  uniun  3954  iunun  4091  iunxun  4092  brun  4183  pwunss  4430  ordsoexmid  4711  onintexmid  4722  dcextest  4730  opthprc  4828  cnvsom  5334  ftpg  5902  tpostpos  6540  eldju  7414  djur  7415  ltexprlemloc  7980  axpre-ltwlin  8256  axpre-apti  8258  axpre-mulext  8261  axpre-suploc  8275  fz01or  10534  cbvsum  12150  fsum3  12178  cbvprod  12349  fprodseq  12374  gcdsupex  12758  gcdsupcl  12759  pythagtriplem2  13073  pythagtrip  13090  wexmiddc  17264