Theorem jaoi 394

Description: Inference disjoining the antecedents of two implications. (Contributed by NM, 5-Apr-1994.)

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		pm2.53 388	. . 3 |- ( ( ph \/ ch ) -> ( -. ph -> ch ) )
2		jaoi.2	. . 3 |- ( ch -> ps )
3	1, 2	syl6 35	. 2 |- ( ( ph \/ ch ) -> ( -. ph -> ps ) )
4		jaoi.1	. 2 |- ( ph -> ps )
5	3, 4	pm2.61d2 172	1 |- ( ( ph \/ ch ) -> ps )

Syntax hints:   -. wn 3   -> wi 4   \/ wo 383

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 385

This theorem is referenced by:  jaod  395  pm1.4  401  jaoa  532  pm1.2  535  orim12i  538  pm1.5  544  pm2.41  597  pm2.42  598  pm2.4  599  pm4.44  601  jaoian  824  jao1i  825  pm3.2ni  899  andi  911  ecase3  982  cases2  993  consensus  999  jaoi3  1011  1fpid3  1029  19.33  1812  19.33b  1813  nfim1  2067  dfsb2  2373  mooran1  2527  2eu3  2555  eueq3  3381  sbcor  3479  sspss  3706  sspsstr  3712  elun  3753  ssun  3792  inss  3842  undif3OLD  3889  ifbi  4107  ifcomnan  4137  elpr2  4199  elpr2OLD  4200  eqoreldifOLD  4226  rabsnifsb  4257  tpprceq3  4335  tppreqb  4336  pwpw0  4344  sssn  4358  snsssn  4372  preq12b  4382  prnebg  4389  elpr2elpr  4398  pwsnALT  4429  prproe  4434  3elpr2eq  4435  unissint  4501  zfpair  4904  propeqop  4970  propssopi  4971  iunopeqop  4981  sotri2  5525  sotri3  5526  somincom  5530  ordelinelOLD  5826  ordssun  5827  onun2i  5843  unizlim  5844  onxpdisj  5847  funtpgOLD  5943  fvfundmfvn0  6226  tpres  6466  sorpssuni  6946  sorpssint  6947  ordeleqon  6988  ordunisuc  7032  orduninsuc  7043  tfinds  7059  limomss  7070  limom  7080  soxp  7290  ressuppssdif  7316  tfr2b  7492  omopthi  7737  domnsym  8086  brwdom  8472  cantnfvalf  8562  iscard3  8916  cflim2  9085  sornom  9099  isfin5  9121  isfin6  9122  sdom2en01  9124  fin23lem29  9163  fin23lem30  9164  fin56  9215  fin67  9217  hsmexlem9  9247  axcc4dom  9263  axdc3lem2  9273  axdc3lem4  9275  brdom3  9350  winainflem  9515  r1tskina  9604  indpi  9729  ltxrlt  10108  ltlen  10138  elnnnn0b  11337  nn0sub  11343  nn0n0n1ge2b  11359  nn0ge2m1nn  11360  xnn0xr  11368  xnn0nemnf  11374  elnn0z  11390  nn0lt10b  11439  nn0le2is012  11441  nn0ind-raph  11477  znnn0nn  11489  uzin  11720  indstr2  11767  nn0ledivnn  11941  xrnemnf  11951  xrnepnf  11952  mnfltxr  11961  xnn0n0n1ge2b  11965  xnn0ge0  11967  nn0pnfge0OLD  11968  xnn0xaddcl  12066  xnn0lenn0nn0  12075  xnn0xadd0  12077  xmullem2  12095  rexmul  12101  xnn0xrge0  12325  elfzonlteqm1  12543  elfznelfzo  12573  injresinjlem  12588  injresinj  12589  fldiv4p1lem1div2  12636  fldiv4lem1div2  12638  modfzo0difsn  12742  ssnn0fi  12784  fsuppmapnn0fiubex  12792  m1expcl2  12882  m1expeven  12907  sq01  12986  nn0opthi  13057  facp1  13065  faclbnd3  13079  faclbnd4lem1  13080  faclbnd4lem3  13082  bcn1  13100  hashnemnf  13132  hashv01gt1  13133  hashneq0  13155  hashrabrsn  13161  hashrabsn01  13162  hashrabsn1  13163  hashunx  13175  hashsnle1  13205  hashfzp1  13218  hash2pwpr  13258  hashge2el2difr  13263  swrdnd2  13433  repswswrd  13531  scshwfzeqfzo  13572  relexpsucr  13769  relexpsucl  13773  relexpcnv  13775  relexprelg  13778  relexpdmg  13782  relexprng  13786  relexpfld  13789  relexpaddg  13793  sumz  14453  arisum  14592  arisum2  14593  ntrivcvg  14629  prod1  14674  fprodfac  14703  mod2eq1n2dvds  15071  mulsucdiv2z  15077  nn0o1gt2  15097  nno  15098  nn0o  15099  sumeven  15110  sumodd  15111  divalglem1  15117  divalglem6  15121  gcdaddmlem  15245  dfgcd2  15263  mulgcd  15265  lcmf  15346  lcmfunsnlem2lem2  15352  lcmfunsnlem2  15353  prm2orodd  15404  dfphi2  15479  nnnn0modprm0  15511  prm23lt5  15519  oddprmdvds  15607  4sqlem19  15667  ramz  15729  prmolefac  15750  prmgaplem7  15761  cshwshashlem1  15802  ressval3d  15937  firest  16093  xpsfeq  16224  xpsfrnel2  16225  funcres2c  16561  symgfix2  17836  pmtrprfval  17907  m1expaddsub  17918  psgnprfval  17941  gsumzunsnd  18355  sralem  19177  0ringnnzr  19269  prmirred  19843  frgpcyg  19922  cnmsgnsubg  19923  psgninv  19928  zrhpsgnelbas  19940  m2detleiblem1  20430  symgmatr01lem  20459  pmatcollpw3fi1  20593  indiscld  20895  pnfnei  21024  mnfnei  21025  alexsubALTlem2  21852  alexsubALTlem3  21853  dscmet  22377  xrtgioo  22609  ishl2  23166  iunmbl2  23325  icombl  23332  ioombl  23333  recnprss  23668  recnperf  23669  dvexp2  23717  dvexp3  23741  dvne0f1  23775  plypf1  23968  taylfvallem1  24111  taylfval  24113  tayl0  24116  coseq0negpitopi  24255  logfac  24347  cxpexp  24414  pythag  24547  reasinsin  24623  harmonicbnd3  24734  lgslem4  25025  gausslemma2dlem0i  25089  lgsquadlem2  25106  2lgslem3  25129  2lgs  25132  2lgsoddprmlem3  25139  cchhllem  25767  lfgrnloop  26020  uhgr2edg  26100  usgredg4  26109  usgredg2v  26119  usgrexmplef  26151  nb3grprlem1  26282  uvtxa01vtx0  26297  wlk1walk  26535  upgriswlk  26537  pthdadjvtx  26626  upgrwlkdvdelem  26632  pthdlem2lem  26663  2pthon3v  26839  clwwlknclwwlkdifs  26873  eupth2lem3lem4  27091  konigsberg  27119  3vfriswmgrlem  27141  1to2vfriswmgr  27143  1to3vfriswmgr  27144  frgrregorufr0  27188  numclwwlkffin0  27215  ex-pr  27287  shunssi  28227  cvmdi  29183  1neg1t1neg1  29514  iundisj2cnt  29558  fz1nnct  29560  xrge0iifiso  29981  esumpr2  30129  measiuns  30280  sxbrsigalem0  30333  bnj964  31013  subfacval3  31171  kur14lem7  31194  mrsubcv  31407  nepss  31599  fz0n  31616  bccolsum  31625  dfon2lem7  31694  trpredlem1  31727  trpred0  31736  sltres  31815  nolesgn2o  31824  nosep1o  31832  altopthsn  32068  elhf2  32282  nn0prpw  32318  dissym1  32420  ordcmp  32446  bj-jaoi1  32556  bj-jaoi2  32557  bj-andnotim  32573  bj-sbsb  32824  finxpreclem2  33227  wl-equsal1i  33329  tan2h  33401  poimirlem23  33432  poimirlem32  33441  itg2addnclem  33461  orfa1  33886  orfa2  33887  inex3  34106  inxpex  34107  elpadd0  35095  hbtlem5  37698  rp-fakeimass  37857  rp-isfinite6  37864  iunrelexp0  37994  relexpss1d  37997  relexpmulg  38002  iunrelexpmin2  38004  relexp01min  38005  relexp0a  38008  relexpxpmin  38009  relexpaddss  38010  clsk1indlem3  38341  ssrecnpr  38507  seff  38508  sblpnf  38509  expgrowthi  38532  dvconstbi  38533  19.33-2  38581  ax6e2ndeq  38775  en3lpVD  39080  undif3VD  39118  ax6e2ndeqVD  39145  ax6e2ndeqALT  39167  iooinlbub  39723  raaan2  41175  2reu3  41188  afvpcfv0  41226  afvfv0bi  41232  afvco2  41256  elprneb  41296  iccpartltu  41361  iccpartgtl  41362  iccpartgt  41363  iccpartleu  41364  iccpartgel  41365  iccpartnel  41374  odz2prm2pw  41475  fmtnofac1  41482  fmtno4prmfac  41484  pwdif  41501  31prm  41512  lighneallem2  41523  lighneallem3  41524  lighneallem4b  41526  lighneallem4  41527  zeo2ALTV  41582  nn0o1gt2ALTV  41605  nn0oALTV  41607  stgoldbwt  41664  sbgoldbwt  41665  sbgoldbalt  41669  sbgoldbm  41672  sbgoldbo  41675  nnsum3primesle9  41682  nnsum4primeseven  41688  nnsum4primesevenALTV  41689  wtgoldbnnsum4prm  41690  bgoldbnnsum3prm  41692  bgoldbtbndlem1  41693  bgoldbtbnd  41697  tgoldbach  41705  tgoldbachOLD  41712  upgrwlkupwlk  41721  elsprel  41725  prsprel  41737  sprsymrelfolem2  41743  ztprmneprm  42125  gsumpr  42139  islinindfis  42238  lindslinindsimp2lem5  42251  lindslinindsimp2  42252  lindsrng01  42257  elfzolborelfzop1  42309  flnn0div2ge  42327  blennn0elnn  42371  blen1b  42382  nnolog2flm1  42384  blengt1fldiv2p1  42387  0dig2pr01  42404  dignn0flhalf  42412  nn0sumshdiglemB  42414  nn0sumshdiglem1  42415