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

Theorem orbi12i 542
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 540 . 2 ((𝜑𝜒) ↔ (𝜑𝜃))
3 orbi12i.1 . . 3 (𝜑𝜓)
43orbi1i 541 . 2 ((𝜑𝜃) ↔ (𝜓𝜃))
52, 4bitri 264 1 ((𝜑𝜒) ↔ (𝜓𝜃))
Colors of variables: wff setvar class
Syntax hints:  wb 196  wo 382
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 384
This theorem is referenced by:  pm4.78  605  andir  930  anddi  932  cases  1011  cases2  1016  dfbi3OLD  1019  4exmidOLD  1022  3orbi123i  1271  3or6  1450  cadcoma  1591  neorian  2917  sspsstri  3742  rexun  3826  elsymdif  3882  symdif2  3885  indi  3906  unab  3927  dfnf5  3985  inundif  4079  dfpr2  4228  ssunsn  4392  ssunpr  4397  sspr  4398  sstp  4399  prneimg  4419  prnebg  4420  pwpr  4462  pwtp  4463  unipr  4481  uniun  4488  iunun  4636  iunxun  4637  brun  4736  zfpair  4934  opthneg  4979  propeqop  4999  pwunss  5048  opthprc  5201  xpeq0  5589  difxp  5593  ordtri2or3  5862  ftpg  6463  ordunpr  7068  mpt2xneldm  7383  tpostpos  7417  oarec  7687  brdom2  8027  modom  8202  dfsup2  8391  wemapsolem  8496  leweon  8872  kmlem16  9025  fin23lem40  9211  axpre-lttri  10024  nn0n0n1ge2b  11397  elnn0z  11428  fz0  12394  sqeqori  13016  hashtpg  13305  cbvsum  14469  cbvprod  14689  rpnnen2lem12  14998  lcmfpr  15387  pythagtriplem2  15569  pythagtrip  15586  mreexexd  16355  mreexexdOLD  16356  cnfldfunALT  19807  ppttop  20859  fixufil  21773  alexsubALTlem2  21899  alexsubALTlem3  21900  alexsubALTlem4  21901  dyaddisj  23410  clwwlkneq0  26990  ofpreima2  29594  odutos  29791  trleile  29794  smatrcl  29990  ordtconnlem1  30098  sitgaddlemb  30538  quad3  31690  nepss  31725  dfso2  31770  dfon2lem4  31815  dfon2lem5  31816  dfon3  32124  brcup  32171  dfrdg4  32183  hfun  32410  bj-dfifc2  32689  bj-eltag  33090  bj-projun  33107  bj-ismooredr2  33190  poimirlem22  33561  poimirlem31  33570  poimirlem32  33571  ispridl2  33967  smprngopr  33981  isdmn3  34003  sbcori  34041  tsbi4  34073  4atlem3  35200  elpadd  35403  paddasslem17  35440  cdlemg31b0N  36299  cdlemg31b0a  36300  cdlemh  36422  jm2.23  37880  ifpim123g  38162  ifpananb  38168  rp-isfinite6  38181  iunrelexp0  38311  clsk1indlem3  38658  aovov0bi  41597  zeoALTV  41906  divgcdoddALTV  41918
  Copyright terms: Public domain W3C validator