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  6539  eldju  7414  djur  7415  ltexprlemloc  7980  axpre-ltwlin  8256  axpre-apti  8258  axpre-mulext  8261  axpre-suploc  8275  fz01or  10535  cbvsum  12151  fsum3  12179  cbvprod  12350  fprodseq  12375  gcdsupex  12759  gcdsupcl  12760  pythagtriplem2  13074  pythagtrip  13091  wexmiddc  17247