Theorem jaod 394

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 393	. 2 ⊢ ((𝜓 ∨ 𝜃) → (𝜑 → 𝜒))
6	5	com12 32	1 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))

Syntax hints:   → wi 4   ∨ wo 382

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 196  df-or 384

This theorem is referenced by:  mpjaod  395  orel2  397  pm2.621  423  jaao  530  jaodan  822  pm2.63  825  ecase2d  978  ecase3d  981  dedlema  993  dedlemb  994  cad0  1547  psssstr  3675  eqoreldif  4172  opthpr  4324  sotric  4985  sotr2  4988  relop  5194  suctr  5725  trsucss  5728  ordelinel  5742  ordelinelOLD  5743  fununi  5878  fnprb  6377  soisoi  6478  ordunisuc2  6936  poxp  7176  soxp  7177  wfrlem14  7315  wfrlem15  7316  tfrlem11  7371  omordi  7533  om00  7542  odi  7546  omeulem2  7550  oewordi  7558  nnmordi  7598  omsmolem  7620  swoord2  7661  nneneq  8028  dffi3  8220  inf3lem6  8413  cantnfle  8451  cantnflem1  8469  cantnflem2  8470  r1sdom  8520  r1ord3g  8525  rankxplim3  8627  carddom2  8686  wdomnumr  8770  alephordi  8780  alephdom  8787  cardaleph  8795  cdainf  8897  cfsuc  8962  cfsmolem  8975  sornom  8982  fin23lem25  9029  fin1a2lem11  9115  fin1a2s  9119  zorn2lem7  9207  ttukeylem5  9218  alephval2  9273  fpwwe2lem13  9343  gch2  9376  gchaclem  9379  prub  9695  sqgt0sr  9806  1re  9918  lelttr  10007  ltletr  10008  letr  10010  mul0or  10546  prodgt0  10747  mulge0b  10772  squeeze0  10805  sup2  10858  un0addcl  11203  un0mulcl  11204  nn0sub  11220  elnnz  11264  zindd  11354  rpneg  11739  xrlttri  11848  xrlelttr  11863  xrltletr  11864  xrletr  11865  qextlt  11908  qextle  11909  xmullem2  11967  xlemul1a  11990  xrsupexmnf  12007  xrinfmexpnf  12008  supxrun  12018  prunioo  12172  difreicc  12175  iccsplit  12176  uzsplit  12281  fzm1  12289  expcl2lem  12734  expeq0  12752  expnegz  12756  expaddz  12766  expmulz  12768  sqlecan  12833  facdiv  12936  facwordi  12938  bcpasc  12970  resqrex  13839  absexpz  13893  caubnd  13946  summo  14295  zsum  14296  zprod  14506  rpnnen2lem12  14793  ordvdsmul  14860  dvdsprime  15238  prmdvdsexpr  15267  prmfac1  15269  pythagtriplem2  15360  4sqlem11  15497  vdwlem6  15528  vdwlem9  15531  vdwlem13  15535  cshwshashlem3  15642  prmlem0  15650  xpscfv  16045  pleval2  16788  pltletr  16794  plelttr  16795  tsrlemax  17043  f1omvdco2  17691  psgnunilem2  17738  efgredlemc  17981  frgpuptinv  18007  lt6abl  18119  dmdprdsplit2lem  18267  drngmul0or  18591  lvecvs0or  18929  domneq0  19118  baspartn  20569  0top  20598  indistopon  20615  restntr  20796  cnindis  20906  cmpfi  21021  filcon  21497  ufprim  21523  ufildr  21545  alexsubALTlem2  21662  alexsubALTlem3  21663  alexsubALTlem4  21664  ovolicc2lem3  23094  rolle  23557  dvivthlem1  23575  coeaddlem  23809  dgrco  23835  plymul0or  23840  aalioulem3  23893  cxpge0  24229  cxpmul2z  24237  cxpcn3lem  24288  scvxcvx  24512  sqf11  24665  ppiublem1  24727  lgsdir2lem2  24851  lgsqrlem2  24872  lmieu  25476  upgredg  25811  frgraogt3nreg  26647  nvmul0or  26889  hvmul0or  27266  disjxpin  28783  subfacp1lem4  30419  untsucf  30841  dfon2lem6  30937  dftrpred3g  30977  nosepon  31066  nodenselem4  31083  broutsideof2  31399  btwnoutside  31402  broutsideof3  31403  outsideoftr  31406  lineunray  31424  lineelsb2  31425  finminlem  31482  nn0prpw  31488  refssfne  31523  meran1  31580  ontgval  31600  ordcmp  31616  bj-sngltag  32164  topdifinfindis  32370  icoreclin  32381  finxpsuclem  32410  poimirlem24  32603  poimirlem25  32604  poimirlem29  32608  poimirlem31  32610  mblfinlem2  32617  ovoliunnfl  32621  itg2addnclem  32631  sdclem2  32708  fdc  32711  divrngidl  32997  lkreqN  33475  cvrnbtwn4  33584  4atlem12  33916  elpaddn0  34104  paddasslem17  34140  paddidm  34145  pmapjoin  34156  llnexchb2  34173  dalawlem13  34187  dalawlem14  34188  dochkrshp4  35696  lcfl6  35807  fphpdo  36399  pellfundex  36468  jm2.19lem4  36577  jm2.26a  36585  relexpmulg  37021  relexp01min  37024  relexpxpmin  37028  relexpaddss  37029  clsk1indlem3  37361  goldbachthlem2  39996  gboge7  40185  bgoldbtbndlem3  40223  eucrct2eupth  41413  av-frgraogt3nreg  41551  lidldomn1  41711  uzlidlring  41719