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

Theorem orbi12i 543
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 541 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 542 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 264 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 383
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 197  df-or 385
This theorem is referenced by:  pm4.78  606  andir  912  anddi  914  cases  992  dfbi3OLD  995  4exmidOLD  998  3orbi123i  1251  3or6  1409  cadcoma  1550  neorian  2887  sspsstri  3707  rexun  3791  elsymdif  3847  symdif2  3850  indi  3871  unab  3892  dfnf5  3950  inundif  4044  dfpr2  4193  ssunsn  4358  ssunpr  4363  sspr  4364  sstp  4365  prneimg  4386  prnebg  4387  pwpr  4428  pwtp  4429  unipr  4447  uniun  4454  iunun  4602  iunxun  4603  brun  4701  zfpair  4902  opthneg  4948  propeqop  4968  pwunss  5017  opthprc  5165  xpeq0  5552  difxp  5556  ordtri2or3  5822  ftpg  6420  ordunpr  7023  mpt2xneldm  7335  tpostpos  7369  oarec  7639  brdom2  7982  modom  8158  dfsup2  8347  wemapsolem  8452  leweon  8831  kmlem16  8984  fin23lem40  9170  axpre-lttri  9983  nn0n0n1ge2b  11356  elnn0z  11387  fz0  12353  sqeqori  12971  hashtpg  13262  cbvsum  14419  cbvprod  14639  rpnnen2lem12  14948  lcmfpr  15334  pythagtriplem2  15516  pythagtrip  15533  mreexexd  16302  mreexexdOLD  16303  cnfldfunALT  19753  ppttop  20805  fixufil  21720  alexsubALTlem2  21846  alexsubALTlem3  21847  alexsubALTlem4  21848  dyaddisj  23358  ofpreima2  29451  odutos  29648  trleile  29651  smatrcl  29847  ordtconnlem1  29955  sitgaddlemb  30395  quad3  31549  nepss  31585  dfso2  31630  dfon2lem4  31675  dfon2lem5  31676  dfon3  31983  brcup  32030  dfrdg4  32042  hfun  32269  bj-dfifc2  32548  bj-eltag  32949  bj-projun  32966  bj-ismooredr2  33049  poimirlem22  33411  poimirlem31  33420  poimirlem32  33421  ispridl2  33817  smprngopr  33831  isdmn3  33853  sbcori  33891  tsbi4  33923  4atlem3  34708  elpadd  34911  paddasslem17  34948  cdlemg31b0N  35808  cdlemg31b0a  35809  cdlemh  35931  jm2.23  37389  ifpim123g  37671  ifpananb  37677  rp-isfinite6  37690  iunrelexp0  37820  clsk1indlem3  38167  aovov0bi  41045  zeoALTV  41352  divgcdoddALTV  41364
  Copyright terms: Public domain W3C validator