Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem jaoi 341

Description: Inference disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaoi.1
jaoi.2

Assertion

Ref	Expression
jaoi

---

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		jaoi.1	. 2
2		jaoi.2	. 2
3		jao 340	. 2
4	1, 2, 3	mp2 43	1

Colors of variables: wff set class

Syntax hints:   wi 3   wo 222

This theorem is referenced by:  pm2.41 342  pm2.42 343  pm2.4 344  pm4.44 345  pm5.63 346  jaoian 425  pm2.64 429  pm2.75 572  pm2.8 574  pm2.82 576  pm5.18 658  orbidi 741  ccase 753  consensus 765  prlem1 768  19.33 1087  19.33b 1088  equvini 1164  dfsb2 1220  mooran1 1418  2eu3 1444  eueq3 1910  sspss 2135  ssnpss 2139  sspsstr 2141  elun 2163  ssun 2196  ifbi 2361  elpr2 2415  pwpw0 2460  sssn 2464  sspr 2466  snsssn 2469  preq12b 2474  iununi 2606  zfpair 2767  opth1 2776  pwundif 2817  ordeleqon 2980  ordssun 3069  ordequn 3070  ordunisuc 3079  onun 3100  unizlim 3103  orduninsuc 3104  onzsl 3107  limomss 3127  limom 3136  tfinds 3151  onxpdisj 3231  erref 4259  domnsym 4443  domsdomtr 4456  rankun 4663  brdom3 4773  iscard3 4860  indpi 5006  prlem934 5111  suppsr2 5195  ltlent 5495  mnfltxrt 5518  addgegt0 5574  msqgt0 5587  mul0or 5663  prodgt0 5775  posex 5856  elnn0z 6094  nn0subt 6108  elnn0nn 6118  nn0ind-raph 6162  exple1t 6538  sumsqne0 6565  sq01t 6582  discrlem 6589  sqrth 6629  sqrcl 6630  sqrge0 6632  leabs 6807  nn0absclt 6816  facp1t 6873  faclbnd3 6884  faclbnd4lem1 6885  faclbnd4lem3 6887  bcpasc 6907  binom 7010  abspef01tlub 7336  efgt0 7345  infxpidmlem4 7498  infxpidmlem7 7501  sn0top 7589  indistop 7590  metxptval 7770  dscmet 7856  efifolem2 8638  shunss 9252  cvmd 10159  neiopne 10369  mapudiscn 10399

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

This theorem depends on definitions:  df-bi 147  df-or 224  df-an 225

Copyright terms: Public domain