Theorem jaod 859

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 18-Aug-1994.)

Hypotheses

Ref	Expression
jaod.1	⊢ (𝜑 → (𝜓 → 𝜒))
jaod.2	⊢ (𝜑 → (𝜃 → 𝜒))

Assertion

Ref	Expression
jaod	⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Proof of Theorem jaod

Step	Hyp	Ref	Expression
1		jaod.1	. . . 4 ⊢ (𝜑 → (𝜓 → 𝜒))
2	1	com12 32	. . 3 ⊢ (𝜓 → (𝜑 → 𝜒))
3		jaod.2	. . . 4 ⊢ (𝜑 → (𝜃 → 𝜒))
4	3	com12 32	. . 3 ⊢ (𝜃 → (𝜑 → 𝜒))
5	2, 4	jaoi 857	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 847

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 207  df-or 848

This theorem is referenced by:  mpjaod  860  orel2  890  pm2.621  898  pm2.63  942  jaao  956  jaodan  959  ecase3d  1034  dedlema  1045  dedlemb  1046  cad0  1618  psssstr  4062  eqoreldif  4639  opthpr  4805  prel12g  4818  opthprneg  4819  axpr  5369  sotric  5561  sotr2  5565  sotr3  5572  relop  5797  suctr  6399  trsucss  6401  ordelinel  6414  fununi  6561  fnprb  7148  soisoi  7269  ordunisuc2  7784  poxp  8068  soxp  8069  frrlem12  8237  frrlem13  8238  tfrlem11  8317  omordi  8491  om00  8500  odi  8504  omeulem2  8508  oewordi  8516  nnmordi  8556  omsmolem  8582  swoord2  8665  nneneq  9130  dffi3  9340  inf3lem6  9548  cantnfle  9586  cantnflem1  9604  cantnflem2  9605  ttrcltr  9631  r1sdom  9689  r1ord3g  9694  rankxplim3  9796  carddom2  9892  wdomnumr  9977  alephordi  9987  alephdom  9994  cardaleph  10002  djuinf  10102  cfsuc  10170  cfsmolem  10183  sornom  10190  fin23lem25  10237  fin1a2lem11  10323  fin1a2s  10327  zorn2lem7  10415  ttukeylem5  10426  alephval2  10485  fpwwe2lem12  10555  gch2  10588  gchaclem  10591  prub  10907  sqgt0sr  11019  1re  11134  lelttr  11224  ltletr  11226  letr  11228  mul0or  11778  prodgt0  11989  mulge0b  12013  squeeze0  12046  sup2  12099  un0addcl  12435  un0mulcl  12436  nn0sub  12452  elnnz  12499  zindd  12595  rpneg  12945  xrlttri  13059  xrlelttr  13076  xrltletr  13077  xrletr  13078  qextlt  13123  qextle  13124  xmullem2  13185  xlemul1a  13208  xrsupexmnf  13225  xrinfmexpnf  13226  supxrun  13236  prunioo  13402  difreicc  13405  iccsplit  13406  uzsplit  13517  fzm1  13528  expcl2lem  13998  expeq0  14017  expnegz  14021  expaddz  14031  expmulz  14033  sqlecan  14134  facdiv  14212  facwordi  14214  bcpasc  14246  resqrex  15175  absexpz  15230  caubnd  15284  summo  15642  zsum  15643  zprod  15862  rpnnen2lem12  16152  ordvdsmul  16229  nn0rppwr  16490  nn0expgcd  16493  dvdsprime  16616  2mulprm  16622  ge2nprmge4  16630  prmdvdsexpr  16646  prmfac1  16649  pythagtriplem2  16747  4sqlem11  16885  vdwlem6  16916  vdwlem9  16919  vdwlem13  16923  cshwshashlem3  17027  prmlem0  17035  pleval2  18259  pltletr  18265  plelttr  18266  tsrlemax  18510  smndex1mgm  18799  f1omvdco2  19345  psgnunilem2  19392  efgredlemc  19642  frgpuptinv  19668  lt6abl  19792  dmdprdsplit2lem  19944  domneq0  20611  drngmul0orOLD  20664  lvecvs0or  21033  baspartn  22857  0top  22886  indistopon  22904  restntr  23085  cnindis  23195  cmpfi  23311  filconn  23786  ufprim  23812  ufildr  23834  alexsubALTlem2  23951  alexsubALTlem3  23952  alexsubALTlem4  23953  ovolicc2lem3  25436  rolle  25910  dvivthlem1  25929  coeaddlem  26170  dgrco  26197  plymul0or  26204  aalioulem3  26258  cxpge0  26608  cxpmul2z  26616  cxpcn3lem  26673  scvxcvx  26912  sqf11  27065  ppiublem1  27129  lgsdir2lem2  27253  lgsqrlem2  27274  2sqnn0  27365  2sqnn  27366  nosepon  27593  nolesgn2ores  27600  nogesgn1ores  27602  nosepne  27608  nolt02o  27623  nosupbnd1lem5  27640  madebdaylemlrcut  27831  madebday  27832  sltlpss  27840  addsproplem2  27900  sleadd1  27919  addsuniflem  27931  mulsproplem9  28050  ssltmul1  28073  ssltmul2  28074  muls0ord  28111  precsexlem9  28140  precsexlem11  28142  recsex  28144  abssnid  28168  sltonold  28185  onnolt  28190  eucliddivs  28288  elnnzs  28312  expsne0  28346  zs12zodd  28377  zs12bday  28379  lmieu  28747  upgrpredgv  29102  edglnl  29106  eucrct2eupth  30207  frgrogt3nreg  30359  nvmul0or  30612  hvmul0or  30987  snsssng  32476  disjxpin  32550  expgt0b  32774  subfacp1lem4  35158  satfvsucsuc  35340  satfrnmapom  35345  sat1el2xp  35354  gonarlem  35369  gonar  35370  goalrlem  35371  goalr  35372  fmlasucdisj  35374  satffunlem1lem1  35377  satffunlem2lem1  35379  untsucf  35685  dfon2lem6  35764  broutsideof2  36098  btwnoutside  36101  broutsideof3  36102  outsideoftr  36105  lineunray  36123  lineelsb2  36124  finminlem  36294  nn0prpw  36299  refssfne  36334  meran1  36387  ontgval  36407  ordcmp  36423  bj-sngltag  36959  bj-prmoore  37091  topdifinfindis  37322  icoreclin  37333  rdgssun  37354  finxpsuclem  37373  poimirlem24  37626  poimirlem25  37627  poimirlem29  37631  poimirlem31  37633  mblfinlem2  37640  ovoliunnfl  37644  itg2addnclem  37653  sdclem2  37724  fdc  37727  divrngidl  38010  lkreqN  39151  cvrnbtwn4  39260  4atlem12  39594  elpaddn0  39782  paddasslem17  39818  paddidm  39823  pmapjoin  39834  llnexchb2  39851  dalawlem13  39865  dalawlem14  39866  dochkrshp4  41371  lcfl6  41482  lcmineqlem  42028  primrootspoweq0  42082  aks6d1c1  42092  sticksstones22  42144  aks6d1c6lem3  42148  oexpreposd  42298  expeqidd  42301  sn-remul0ord  42384  sn-sup2  42467  fphpdo  42793  pellfundex  42862  jm2.19lem4  42968  jm2.26a  42976  ordnexbtwnsuc  43243  onov0suclim  43250  oege2  43283  succlg  43304  dflim5  43305  oacl2g  43306  omcl2  43309  omcl3g  43310  naddgeoa  43370  safesnsupfiss  43391  fzunt  43431  fzuntd  43432  fzunt1d  43433  fzuntgd  43434  relexpmulg  43686  relexp01min  43689  relexpxpmin  43693  relexpaddss  43694  clsk1indlem3  44019  or2expropbi  47022  ich2exprop  47459  poprelb  47512  reuopreuprim  47514  goldbachthlem2  47534  requad01  47609  evenltle  47705  gbowge7  47751  bgoldbtbndlem3  47795  elclnbgrelnbgr  47813  clnbgrel  47816  dfclnbgr6  47844  dfnbgr6  47845  dfsclnbgr6  47846  upgrimpths  47897  clnbgrgrim  47922  isubgr3stgrlem4  47957  isubgr3stgrlem7  47960  grlimgredgex  47988  gpgedgvtx1  48050  gpgvtxedg0  48051  gpgvtxedg1  48052  lidldomn1  48219  uzlidlring  48223  prelrrx2b  48703  line2y  48744  itschlc0xyqsol1  48755  itsclc0xyqsolr  48758  inlinecirc02plem  48775