ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  jaoi Unicode version

Theorem jaoi 669
Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.) (Revised by NM, 31-Jan-2015.)
Hypotheses
Ref Expression
jaoi.1  |-  ( ph  ->  ps )
jaoi.2  |-  ( ch 
->  ps )
Assertion
Ref Expression
jaoi  |-  ( (
ph  \/  ch )  ->  ps )

Proof of Theorem jaoi
StepHypRef Expression
1 jaoi.1 . 2  |-  ( ph  ->  ps )
2 jaoi.2 . 2  |-  ( ch 
->  ps )
3 pm3.44 668 . 2  |-  ( ( ( ph  ->  ps )  /\  ( ch  ->  ps ) )  ->  (
( ph  \/  ch )  ->  ps ) )
41, 2, 3mp2an 417 1  |-  ( (
ph  \/  ch )  ->  ps )
Colors of variables: wff set class
Syntax hints:    -> wi 4    \/ wo 662
This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 104  ax-ia2 105  ax-ia3 106  ax-io 663
This theorem depends on definitions:  df-bi 115
This theorem is referenced by:  jaod  670  jaoa  673  pm2.53  674  pm1.4  679  imorri  701  ioran  702  pm3.14  703  pm1.2  706  orim12i  709  pm1.5  715  pm2.41  726  pm2.42  727  pm2.4  728  pm4.44  729  jaoian  742  jao1i  743  pm2.64  748  pm2.76  755  pm2.82  759  pm3.2ni  760  andi  765  condc  783  pm2.61ddc  792  pm5.18dc  811  dcim  818  imorr  831  pm4.78i  842  pm2.85dc  845  peircedc  854  dcan  876  dcor  877  pm4.42r  913  oplem1  917  xoranor  1309  biassdc  1327  anxordi  1332  19.33  1414  hbequid  1447  hbor  1479  19.30dc  1559  19.43  1560  19.32r  1611  hbae  1647  equvini  1682  equveli  1683  exdistrfor  1722  dveeq2  1737  dveeq2or  1738  sbequi  1761  nfsbxy  1860  nfsbxyt  1861  sbcomxyyz  1888  dvelimALT  1928  dvelimfv  1929  dvelimor  1936  modc  1985  mooran1  2014  moexexdc  2026  rgen2a  2418  r19.32r  2502  eueq2dc  2766  eueq3dc  2767  sbcor  2859  elun  3114  ssun  3152  inss  3202  undif3ss  3232  ifsbdc  3371  elpr2  3428  sssnr  3553  ssprr  3556  sstpr  3557  preq12b  3570  copsexg  4007  sotritric  4087  regexmidlem1  4284  nn0eln0  4367  xpeq0r  4776  funtpg  4981  acexmidlemcase  5538  acexmidlem2  5540  nnm00  6168  renfdisj  7239  nn0ge0  8380  elnnnn0b  8399  xnn0xr  8423  xnn0nemnf  8429  elnn0z  8445  nn0n0n1ge2b  8508  nn0ind-raph  8545  uzin  8732  elnn1uz2  8775  indstr2  8777  nn0ledivnn  8919  xrnemnf  8929  xrnepnf  8930  mnfltxr  8937  nn0pnfge0  8942  elfzonlteqm1  9296  fldiv4p1lem1div2  9387  flqeqceilz  9400  modfzo0difsn  9477  m1expcl2  9595  m1expeven  9620  facp1  9754  faclbnd3  9767  bcn1  9782  sizeinfuni  9801  mulsucdiv2z  10429  nn0o1gt2  10449  nno  10450  nn0o  10451  dfgcd2  10547  mulgcd  10549  gcdmultiplez  10554  dvdssq  10564  cncongr2  10630  prm2orodd  10652  bj-nn0suc  10917  bj-inf2vnlem2  10924  bj-nn0sucALT  10931
  Copyright terms: Public domain W3C validator