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

Theorem orbi12i 541
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 539 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 540 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 262 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 194  wo 381
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 195  df-or 383
This theorem is referenced by:  pm4.78  603  andir  907  anddi  909  dfbi3  932  4exmid  976  cases  1003  3orbi123i  1244  3or6  1401  cadcoma  1541  neorian  2871  sspsstri  3666  rexun  3750  elsymdif  3806  symdif2  3809  indi  3827  unab  3848  dfnf5  3901  inundif  3993  dfpr2  4138  ssunsn  4293  ssunpr  4296  sspr  4297  sstp  4298  prneimg  4319  prnebg  4320  pwpr  4358  pwtp  4359  unipr  4375  uniun  4382  iunun  4530  iunxun  4531  brun  4623  zfpair  4822  opthneg  4866  pwunss  4929  opthprc  5075  xpeq0  5455  difxp  5459  ordtri2or3  5723  ftpg  6302  ordunpr  6891  mpt2xneldm  7198  tpostpos  7232  oarec  7502  brdom2  7844  modom  8019  dfsup2  8206  wemapsolem  8311  leweon  8690  kmlem16  8843  fin23lem40  9029  axpre-lttri  9838  nn0n0n1ge2b  11202  elnn0z  11219  fz0  12178  sqeqori  12789  hashtpg  13067  cbvsum  14215  cbvprod  14426  rpnnen2lem12  14735  lcmfpr  15120  pythagtriplem2  15302  pythagtrip  15319  mreexexd  16073  mreexexdOLD  16074  ppttop  20559  fixufil  21474  alexsubALTlem2  21600  alexsubALTlem3  21601  alexsubALTlem4  21602  dyaddisj  23083  ofpreima2  28651  odutos  28796  trleile  28799  smatrcl  28992  ordtconlem1  29100  sitgaddlemb  29539  quad3  30620  nepss  30656  dfso2  30699  dfon2lem4  30737  dfon2lem5  30738  nofulllem5  30907  dfon3  30971  brcup  31018  dfrdg4  31030  hfun  31257  bj-dfifc2  31536  bj-eltag  31957  bj-projun  31974  poimirlem22  32400  poimirlem31  32409  poimirlem32  32410  ispridl2  32806  smprngopr  32820  isdmn3  32842  sbcori  32880  tsbi4  32912  4atlem3  33699  elpadd  33902  paddasslem17  33939  cdlemg31b0N  34799  cdlemg31b0a  34800  cdlemh  34922  jm2.23  36380  ifpim123g  36663  ifpananb  36669  rp-isfinite6  36682  iunrelexp0  36812  clsk1indlem3  37160  aovov0bi  39726  zeoALTV  39920  divgcdoddALTV  39932  propeqop  40122
  Copyright terms: Public domain W3C validator