Theorem orbi12i 714

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

Syntax hints:   <-> wb 103   \/ wo 662

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

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  andir  766  anddi  768  dcbii  781  3orbi123i  1129  3or6  1255  excxor  1310  19.33b2  1561  sbequilem  1760  sborv  1812  sbor  1870  r19.43  2513  rexun  3153  indi  3218  difindiss  3225  symdifxor  3237  unab  3238  dfpr2  3425  rabrsndc  3468  pwprss  3605  pwtpss  3606  unipr  3623  uniun  3628  iunun  3763  iunxun  3764  brun  3839  pwunss  4046  ordsoexmid  4313  onintexmid  4323  opthprc  4417  cnvsom  4891  ftpg  5379  tpostpos  5913  ltexprlemloc  6859  axpre-ltwlin  7111  axpre-apti  7113  axpre-mulext  7116  fz01or  9204  gcdsupex  10493  gcdsupcl  10494