Theorem orbi12i 521

Description: Infer the disjunction of two equivalences. (Contributed by NM, 3-Jan-1993.)

Hypotheses

Ref	Expression
orbi12i.1
orbi12i.2

Assertion

Ref	Expression
orbi12i

Proof of Theorem orbi12i

Step	Hyp	Ref	Expression
1		orbi12i.2	. . 3
2	1	orbi2i 519	. 2
3		orbi12i.1	. . 3
4	3	orbi1i 520	. 2
5	2, 4	bitri 249	1

Syntax hints:  <->wb 184  \/wo 368

This theorem is referenced by:  pm4.78  582  andir  868  anddi  870  dfbi3  893  4exmid  939  cases  970  3orbi123i  1186  3or6  1310  cadcoma  1462  neorian  2784  sspsstri  3605  rexun  3683  indi  3743  symdif2  3763  unab  3764  inundif  3906  dfpr2  4044  ssunsn  4190  ssunpr  4192  sspr  4193  sstp  4194  prneimg  4211  prnebg  4212  pwpr  4245  pwtp  4246  unipr  4262  uniun  4268  iunun  4411  iunxun  4412  brun  4500  zfpair  4689  pwunss  4790  ordtri2or3  4980  opthprc  5052  xpeq0  5432  difxp  5436  ftpg  6081  ordunpr  6661  tpostpos  6994  oarec  7230  brdom2  7565  modom  7740  dfsup2  7922  wemapsolem  7996  leweon  8410  kmlem16  8566  fin23lem40  8752  axpre-lttri  9563  nn0n0n1ge2b  10885  elnn0z  10902  fz0  11730  sqeqori  12280  hashtpg  12523  cbvsum  13517  cbvprod  13722  rpnnen2  13959  pythagtriplem2  14341  pythagtrip  14358  mreexexd  15045  ppttop  19508  fixufil  20423  alexsubALTlem2  20548  alexsubALTlem3  20549  alexsubALTlem4  20550  dyaddisj  22005  ofpreima2  27508  odutos  27651  trleile  27654  ordtconlem1  27906  quad3  29024  nepss  29095  dfso2  29183  dfon2lem4  29218  dfon2lem5  29219  nofulllem5  29466  elsymdif  29473  dfon3  29542  brcup  29589  dfrdg4  29600  hfun  29835  ispridl2  30435  smprngopr  30449  isdmn3  30471  sbcori  30511  tsbi4  30543  jm2.23  30938  aovov0bi  32281  bj-dfifc2  34164  bj-eltag  34535  bj-projun  34552  4atlem3  35320  elpadd  35523  paddasslem17  35560  cdlemg31b0N  36420  cdlemg31b0a  36421  cdlemh  36543  bj-ifim123g  37706  bj-ifananb  37731  rp-isfinite6  37744

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 185  df-or 370