Theorem orbi12i 713

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

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

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 662

This theorem depends on definitions:  df-bi 115

This theorem is referenced by:  andir  765  anddi  767  dcbii  780  3orbi123i  1128  3or6  1254  excxor  1309  19.33b2  1560  sbequilem  1759  sborv  1811  sbor  1869  r19.43  2512  rexun  3152  indi  3211  difindiss  3218  symdifxor  3230  unab  3231  dfpr2  3417  rabrsndc  3460  pwprss  3597  pwtpss  3598  unipr  3615  uniun  3620  iunun  3755  iunxun  3756  brun  3831  pwunss  4038  ordsoexmid  4305  onintexmid  4315  opthprc  4409  cnvsom  4881  ftpg  5368  tpostpos  5902  ltexprlemloc  6797  axpre-ltwlin  7049  axpre-apti  7051  axpre-mulext  7054  fz01or  10278  gcdsupex  10349  gcdsupcl  10350