Theorem jaoi 275

Description: Inference disjoining the antecedents of two implications.

Hypotheses

Ref	Expression
jaoi.1	|- (ph -> ps)
jaoi.2	|- (ch -> ps)

Assertion

Ref	Expression
jaoi	|- ((ph \/ ch) -> ps)

Proof of Theorem jaoi

Step	Hyp	Ref	Expression
1		jaoi.1	. 2 |- (ph -> ps)
2		jaoi.2	. 2 |- (ch -> ps)
3		jao 274	. 2 |- ((ph -> ps) -> ((ch -> ps) -> ((ph \/ ch) -> ps)))
4	1, 2, 3	mp2 43	1 |- ((ph \/ ch) -> ps)

Syntax hints:   -> wi 2   \/ wo 195

This theorem is referenced by:  pm5.18 497  orbidi 510  ccase 562  consensus 574  prlem1 576  19.33 770  19.33b 771  eqvin.l1 851  mooran1 1049  2eu3 1069  eueq3 1430  sspss 1569  ssnpss 1573  sspsstr 1575  elun 1601  ssun 1634  ifbi 1783  sssn 1852  preq12b 1874  pwpw0 1883  zfpair 1891  prex 1892  opth 1898  iununi 2037  ordeleqon 2241  ordssun 2330  ordequn 2331  ordunisuc 2339  onun 2358  limsuc 2361  unizlim 2364  orduninsuc 2365  onzsl 2367  limomss 2378  limom 2387  tfinds 2401  onxpdisj 2476  erref 3212  domnsym 3365  domsdomtr 3374  phplem4 3406  ssnn 3429  rankun 3535  iscard3 3693  indpi 3828  prlem934 3933  suppsr2 4017  mul0or 4210  ltlent 4288  addgegt0 4325  sqgt0 4343  posex 4422  elnn0z 4574  nn0subt 4587  elnn0nn 4593  nn0ind 4612  discrlem 4716  sqrth 4757  sqrcl 4758  sqrge0 4760  leabs 4852  facp1t 4873  infxpidmlem4 4936  infxpidmlem7 4939  shunss 5338  mdsym 5784

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

This theorem depends on definitions:  df-bi 128  df-or 197  df-an 198

metamath.org