Theorem orbi12i 753

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

Syntax hints:   <-> wb 104   \/ wo 697

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-io 698

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  808  anddi  810  3orbi123i  1171  3or6  1301  excxor  1356  19.33b2  1608  sbequilem  1810  sborv  1862  sbor  1927  r19.43  2589  rexun  3256  indi  3323  difindiss  3330  symdifxor  3342  unab  3343  dfpr2  3546  rabrsndc  3591  pwprss  3732  pwtpss  3733  unipr  3750  uniun  3755  iunun  3891  iunxun  3892  brun  3979  pwunss  4205  ordsoexmid  4477  onintexmid  4487  dcextest  4495  opthprc  4590  cnvsom  5082  ftpg  5604  tpostpos  6161  eldju  6953  djur  6954  ltexprlemloc  7415  axpre-ltwlin  7691  axpre-apti  7693  axpre-mulext  7696  axpre-suploc  7710  fz01or  9891  cbvsum  11129  fsum3  11156  cbvprod  11327  gcdsupex  11646  gcdsupcl  11647