MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  orbi12i Structured version   Visualization version   GIF version

Theorem orbi12i 912
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
StepHypRef Expression
1 orbi12i.2 . . 3 (𝜒𝜃)
21orbi2i 910 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 911 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 278 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 209  wo 844
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 210  df-or 845
This theorem is referenced by:  pm4.78  932  andir  1006  anddi  1008  cases  1038  cases2  1043  3orbi123i  1153  3or6  1444  noran  1527  noranOLD  1528  cadcoma  1614  neorian  3107  sspsstri  4063  rexun  4150  elsymdif  4207  indi  4233  unab  4253  dfnf5  4315  inundif  4408  dfpr2  4567  ssunsn  4742  ssunpr  4746  sspr  4747  sstp  4748  prneimg  4766  prnebg  4767  pwpr  4813  pwtp  4814  unipr  4836  uniun  4842  iunun  4996  iunxun  4997  brun  5098  zfpair  5303  opthneg  5354  propeqop  5378  pwunssOLD  5436  opthprc  5597  dmopab2rex  5767  xpeq0  5998  difxp  6002  ordtri2or3  6269  ftpg  6899  ordunpr  7524  mpoxneldm  7861  tpostpos  7895  oarec  8171  brdom2  8522  modom  8703  dfsup2  8892  wemapsolem  8998  djuunxp  9334  leweon  9422  kmlem16  9576  fin23lem40  9758  axpre-lttri  10572  nn0n0n1ge2b  11949  elnn0z  11980  fz0  12915  sqeqori  13570  hashtpg  13837  swrdnnn0nd  14007  swrdnd0  14008  cbvsum  15041  cbvprod  15258  rpnnen2lem12  15567  lcmfpr  15958  pythagtriplem2  16141  pythagtrip  16158  mreexexd  16908  smndex1basss  18059  smndex1mgm  18061  smndex1n0mnd  18066  cnfldfunALT  20544  ppttop  21601  fixufil  22516  alexsubALTlem2  22642  alexsubALTlem3  22643  alexsubALTlem4  22644  dyaddisj  24189  clwwlkneq0  27803  ofpreima2  30408  odutos  30647  trleile  30650  prmidl2  30978  smatrcl  31082  ordtconnlem1  31185  sitgaddlemb  31624  satfvsuclem2  32625  satfvsucsuc  32630  satfdm  32634  satf0  32637  satffunlem2lem1  32669  dmopab3rexdif  32670  quad3  32931  nepss  32966  dfso2  33008  dfon2lem4  33049  dfon2lem5  33050  frrlem13  33153  dfon3  33371  brcup  33418  dfrdg4  33430  hfun  33657  bj-df-ifc  33931  bj-eltag  34317  bj-projun  34334  poimirlem22  34979  poimirlem31  34988  poimirlem32  34989  ispridl2  35376  smprngopr  35390  isdmn3  35412  sbcori  35447  tsbi4  35474  4atlem3  36792  elpadd  36995  paddasslem17  37032  cdlemg31b0N  37890  cdlemg31b0a  37891  cdlemh  38013  jm2.23  39769  ifpim123g  40040  ifpananb  40046  rp-isfinite6  40058  iunrelexp0  40235  clsk1indlem3  40581  aovov0bi  43594  zeoALTV  44030  divgcdoddALTV  44042  rrx2pnedifcoorneor  44960  line2xlem  44997
  Copyright terms: Public domain W3C validator