Theorem orbi12i 754

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

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

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 699

This theorem depends on definitions:  df-bi 116

This theorem is referenced by:  andir  809  anddi  811  3orbi123i  1179  3or6  1313  excxor  1368  19.33b2  1617  sbequilem  1826  sborv  1878  sbor  1942  r19.43  2623  rexun  3301  indi  3368  difindiss  3375  symdifxor  3387  unab  3388  dfpr2  3594  rabrsndc  3643  pwprss  3784  pwtpss  3785  unipr  3802  uniun  3807  iunun  3943  iunxun  3944  brun  4032  pwunss  4260  ordsoexmid  4538  onintexmid  4549  dcextest  4557  opthprc  4654  cnvsom  5146  ftpg  5668  tpostpos  6228  eldju  7029  djur  7030  ltexprlemloc  7544  axpre-ltwlin  7820  axpre-apti  7822  axpre-mulext  7825  axpre-suploc  7839  fz01or  10042  cbvsum  11297  fsum3  11324  cbvprod  11495  fprodseq  11520  gcdsupex  11886  gcdsupcl  11887  pythagtriplem2  12194  pythagtrip  12211