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  1172  3or6  1302  excxor  1357  19.33b2  1609  sbequilem  1811  sborv  1863  sbor  1928  r19.43  2592  rexun  3261  indi  3328  difindiss  3335  symdifxor  3347  unab  3348  dfpr2  3551  rabrsndc  3599  pwprss  3740  pwtpss  3741  unipr  3758  uniun  3763  iunun  3899  iunxun  3900  brun  3987  pwunss  4213  ordsoexmid  4485  onintexmid  4495  dcextest  4503  opthprc  4598  cnvsom  5090  ftpg  5612  tpostpos  6169  eldju  6961  djur  6962  ltexprlemloc  7439  axpre-ltwlin  7715  axpre-apti  7717  axpre-mulext  7720  axpre-suploc  7734  fz01or  9922  cbvsum  11161  fsum3  11188  cbvprod  11359  fprodseq  11384  gcdsupex  11682  gcdsupcl  11683