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  785  pm2.61ddc  794  pm5.18dc  813  dcim  820  imorr  833  pm4.78i  844  pm2.85dc  847  peircedc  856  dcan  878  dcor  879  pm4.42r  915  oplem1  919  xoranor  1311  biassdc  1329  anxordi  1334  19.33  1416  hbequid  1449  hbor  1481  19.30dc  1561  19.43  1562  19.32r  1613  hbae  1650  equvini  1685  equveli  1686  exdistrfor  1725  dveeq2  1740  dveeq2or  1741  sbequi  1764  nfsbxy  1863  nfsbxyt  1864  sbcomxyyz  1891  dvelimALT  1931  dvelimfv  1932  dvelimor  1939  modc  1988  mooran1  2017  moexexdc  2029  rgen2a  2425  r19.32r  2510  eueq2dc  2779  eueq3dc  2780  sbcor  2872  elun  3130  ssun  3168  inss  3218  undif3ss  3249  ifsbdc  3391  ifiddc  3410  eqifdc  3411  ifandc  3413  elpr2  3453  sssnr  3582  ssprr  3585  sstpr  3586  preq12b  3599  copsexg  4047  sotritric  4127  regexmidlem1  4324  nn0eln0  4408  xpeq0r  4822  funtpg  5032  acexmidlemcase  5610  acexmidlem2  5612  nnm00  6242  djuss  6708  eldju2ndl  6710  eldju2ndr  6711  updjud  6720  exmidfodomrlemim  6774  renfdisj  7493  nn0ge0  8634  elnnnn0b  8653  xnn0xr  8677  xnn0nemnf  8683  elnn0z  8699  nn0n0n1ge2b  8762  nn0ind-raph  8799  uzin  8986  elnn1uz2  9029  indstr2  9031  nn0ledivnn  9173  xrnemnf  9183  xrnepnf  9184  mnfltxr  9191  nn0pnfge0  9196  elfzonlteqm1  9552  fldiv4p1lem1div2  9643  flqeqceilz  9656  modfzo0difsn  9733  m1expcl2  9879  m1expeven  9904  facp1  10038  faclbnd3  10051  bcn1  10066  hashinfuni  10085  hashfzp1  10132  isumz  10672  mulsucdiv2z  10791  nn0o1gt2  10811  nno  10812  nn0o  10813  dfgcd2  10909  mulgcd  10911  gcdmultiplez  10916  dvdssq  10926  cncongr2  10992  prm2orodd  11014  dfphi2  11102  bj-nn0suc  11328  bj-inf2vnlem2  11335  bj-nn0sucALT  11342  el2oss1o  11356
  Copyright terms: Public domain W3C validator