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  1619  psssstr  4058  eqoreldif  4639  opthpr  4804  prel12g  4817  opthprneg  4818  axpr  5369  sotric  5559  sotr2  5563  sotr3  5570  relop  5796  suctr  6401  trsucss  6403  ordelinel  6416  fununi  6563  fnprb  7150  soisoi  7270  ordunisuc2  7782  poxp  8066  soxp  8067  frrlem12  8235  frrlem13  8236  tfrlem11  8315  omordi  8489  om00  8498  odi  8502  omeulem2  8506  oewordi  8514  nnmordi  8554  omsmolem  8580  swoord2  8663  nneneq  9124  dffi3  9324  inf3lem6  9532  cantnfle  9570  cantnflem1  9588  cantnflem2  9589  ttrcltr  9615  r1sdom  9676  r1ord3g  9681  rankxplim3  9783  carddom2  9879  wdomnumr  9964  alephordi  9974  alephdom  9981  cardaleph  9989  djuinf  10089  cfsuc  10157  cfsmolem  10170  sornom  10177  fin23lem25  10224  fin1a2lem11  10310  fin1a2s  10314  zorn2lem7  10402  ttukeylem5  10413  alephval2  10472  fpwwe2lem12  10542  gch2  10575  gchaclem  10578  prub  10894  sqgt0sr  11006  1re  11121  lelttr  11212  ltletr  11214  letr  11216  mul0or  11766  prodgt0  11977  mulge0b  12001  squeeze0  12034  sup2  12087  un0addcl  12423  un0mulcl  12424  nn0sub  12440  elnnz  12487  zindd  12582  rpneg  12928  xrlttri  13042  xrlelttr  13059  xrltletr  13060  xrletr  13061  qextlt  13106  qextle  13107  xmullem2  13168  xlemul1a  13191  xrsupexmnf  13208  xrinfmexpnf  13209  supxrun  13219  prunioo  13385  difreicc  13388  iccsplit  13389  uzsplit  13500  fzm1  13511  expcl2lem  13984  expeq0  14003  expnegz  14007  expaddz  14017  expmulz  14019  sqlecan  14120  facdiv  14198  facwordi  14200  bcpasc  14232  resqrex  15161  absexpz  15216  caubnd  15270  summo  15628  zsum  15629  zprod  15848  rpnnen2lem12  16138  ordvdsmul  16215  nn0rppwr  16476  nn0expgcd  16479  dvdsprime  16602  2mulprm  16608  ge2nprmge4  16616  prmdvdsexpr  16632  prmfac1  16635  pythagtriplem2  16733  4sqlem11  16871  vdwlem6  16902  vdwlem9  16905  vdwlem13  16909  cshwshashlem3  17013  prmlem0  17021  pleval2  18245  pltletr  18251  plelttr  18252  tsrlemax  18496  smndex1mgm  18819  f1omvdco2  19364  psgnunilem2  19411  efgredlemc  19661  frgpuptinv  19687  lt6abl  19811  dmdprdsplit2lem  19963  domneq0  20627  drngmul0orOLD  20680  lvecvs0or  21049  baspartn  22872  0top  22901  indistopon  22919  restntr  23100  cnindis  23210  cmpfi  23326  filconn  23801  ufprim  23827  ufildr  23849  alexsubALTlem2  23966  alexsubALTlem3  23967  alexsubALTlem4  23968  ovolicc2lem3  25450  rolle  25924  dvivthlem1  25943  coeaddlem  26184  dgrco  26211  plymul0or  26218  aalioulem3  26272  cxpge0  26622  cxpmul2z  26630  cxpcn3lem  26687  scvxcvx  26926  sqf11  27079  ppiublem1  27143  lgsdir2lem2  27267  lgsqrlem2  27288  2sqnn0  27379  2sqnn  27380  nosepon  27607  nolesgn2ores  27614  nogesgn1ores  27616  nosepne  27622  nolt02o  27637  nosupbnd1lem5  27654  madebdaylemlrcut  27847  madebday  27848  sltlpss  27856  addsproplem2  27916  sleadd1  27935  addsuniflem  27947  mulsproplem9  28066  ssltmul1  28089  ssltmul2  28090  muls0ord  28127  precsexlem9  28156  precsexlem11  28158  recsex  28160  abssnid  28184  sltonold  28201  onnolt  28206  eucliddivs  28304  elnnzs  28328  expsne0  28362  zs12zodd  28395  zs12bday  28397  lmieu  28765  upgrpredgv  29121  edglnl  29125  eucrct2eupth  30229  frgrogt3nreg  30381  nvmul0or  30634  hvmul0or  31009  snsssng  32498  disjxpin  32572  expgt0b  32806  subfacp1lem4  35250  satfvsucsuc  35432  satfrnmapom  35437  sat1el2xp  35446  gonarlem  35461  gonar  35462  goalrlem  35463  goalr  35464  fmlasucdisj  35466  satffunlem1lem1  35469  satffunlem2lem1  35471  untsucf  35777  dfon2lem6  35853  broutsideof2  36189  btwnoutside  36192  broutsideof3  36193  outsideoftr  36196  lineunray  36214  lineelsb2  36215  finminlem  36385  nn0prpw  36390  refssfne  36425  meran1  36478  ontgval  36498  ordcmp  36514  bj-sngltag  37050  bj-prmoore  37182  topdifinfindis  37413  icoreclin  37424  rdgssun  37445  finxpsuclem  37464  poimirlem24  37707  poimirlem25  37708  poimirlem29  37712  poimirlem31  37714  mblfinlem2  37721  ovoliunnfl  37725  itg2addnclem  37734  sdclem2  37805  fdc  37808  divrngidl  38091  lkreqN  39292  cvrnbtwn4  39401  4atlem12  39734  elpaddn0  39922  paddasslem17  39958  paddidm  39963  pmapjoin  39974  llnexchb2  39991  dalawlem13  40005  dalawlem14  40006  dochkrshp4  41511  lcfl6  41622  lcmineqlem  42168  primrootspoweq0  42222  aks6d1c1  42232  sticksstones22  42284  aks6d1c6lem3  42288  oexpreposd  42443  expeqidd  42446  sn-remul0ord  42529  sn-sup2  42612  fphpdo  42937  pellfundex  43006  jm2.19lem4  43112  jm2.26a  43120  ordnexbtwnsuc  43387  onov0suclim  43394  oege2  43427  succlg  43448  dflim5  43449  oacl2g  43450  omcl2  43453  omcl3g  43454  naddgeoa  43514  safesnsupfiss  43535  fzunt  43575  fzuntd  43576  fzunt1d  43577  fzuntgd  43578  relexpmulg  43830  relexp01min  43833  relexpxpmin  43837  relexpaddss  43838  clsk1indlem3  44163  or2expropbi  47161  ich2exprop  47598  poprelb  47651  reuopreuprim  47653  goldbachthlem2  47673  requad01  47748  evenltle  47844  gbowge7  47890  bgoldbtbndlem3  47934  elclnbgrelnbgr  47952  clnbgrel  47955  dfclnbgr6  47983  dfnbgr6  47984  dfsclnbgr6  47985  upgrimpths  48036  clnbgrgrim  48061  isubgr3stgrlem4  48096  isubgr3stgrlem7  48099  grlimgredgex  48127  gpgedgvtx1  48189  gpgvtxedg0  48190  gpgvtxedg1  48191  lidldomn1  48358  uzlidlring  48362  prelrrx2b  48842  line2y  48883  itschlc0xyqsol1  48894  itsclc0xyqsolr  48897  inlinecirc02plem  48914