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  4059  eqoreldif  4638  opthpr  4803  prel12g  4816  opthprneg  4817  axpr  5365  sotric  5554  sotr2  5558  sotr3  5565  relop  5790  suctr  6394  trsucss  6396  ordelinel  6409  fununi  6556  fnprb  7142  soisoi  7262  ordunisuc2  7774  poxp  8058  soxp  8059  frrlem12  8227  frrlem13  8228  tfrlem11  8307  omordi  8481  om00  8490  odi  8494  omeulem2  8498  oewordi  8506  nnmordi  8546  omsmolem  8572  swoord2  8655  nneneq  9115  dffi3  9315  inf3lem6  9523  cantnfle  9561  cantnflem1  9579  cantnflem2  9580  ttrcltr  9606  r1sdom  9667  r1ord3g  9672  rankxplim3  9774  carddom2  9870  wdomnumr  9955  alephordi  9965  alephdom  9972  cardaleph  9980  djuinf  10080  cfsuc  10148  cfsmolem  10161  sornom  10168  fin23lem25  10215  fin1a2lem11  10301  fin1a2s  10305  zorn2lem7  10393  ttukeylem5  10404  alephval2  10463  fpwwe2lem12  10533  gch2  10566  gchaclem  10569  prub  10885  sqgt0sr  10997  1re  11112  lelttr  11203  ltletr  11205  letr  11207  mul0or  11757  prodgt0  11968  mulge0b  11992  squeeze0  12025  sup2  12078  un0addcl  12414  un0mulcl  12415  nn0sub  12431  elnnz  12478  zindd  12574  rpneg  12924  xrlttri  13038  xrlelttr  13055  xrltletr  13056  xrletr  13057  qextlt  13102  qextle  13103  xmullem2  13164  xlemul1a  13187  xrsupexmnf  13204  xrinfmexpnf  13205  supxrun  13215  prunioo  13381  difreicc  13384  iccsplit  13385  uzsplit  13496  fzm1  13507  expcl2lem  13980  expeq0  13999  expnegz  14003  expaddz  14013  expmulz  14015  sqlecan  14116  facdiv  14194  facwordi  14196  bcpasc  14228  resqrex  15157  absexpz  15212  caubnd  15266  summo  15624  zsum  15625  zprod  15844  rpnnen2lem12  16134  ordvdsmul  16211  nn0rppwr  16472  nn0expgcd  16475  dvdsprime  16598  2mulprm  16604  ge2nprmge4  16612  prmdvdsexpr  16628  prmfac1  16631  pythagtriplem2  16729  4sqlem11  16867  vdwlem6  16898  vdwlem9  16901  vdwlem13  16905  cshwshashlem3  17009  prmlem0  17017  pleval2  18241  pltletr  18247  plelttr  18248  tsrlemax  18492  smndex1mgm  18815  f1omvdco2  19361  psgnunilem2  19408  efgredlemc  19658  frgpuptinv  19684  lt6abl  19808  dmdprdsplit2lem  19960  domneq0  20624  drngmul0orOLD  20677  lvecvs0or  21046  baspartn  22870  0top  22899  indistopon  22917  restntr  23098  cnindis  23208  cmpfi  23324  filconn  23799  ufprim  23825  ufildr  23847  alexsubALTlem2  23964  alexsubALTlem3  23965  alexsubALTlem4  23966  ovolicc2lem3  25448  rolle  25922  dvivthlem1  25941  coeaddlem  26182  dgrco  26209  plymul0or  26216  aalioulem3  26270  cxpge0  26620  cxpmul2z  26628  cxpcn3lem  26685  scvxcvx  26924  sqf11  27077  ppiublem1  27141  lgsdir2lem2  27265  lgsqrlem2  27286  2sqnn0  27377  2sqnn  27378  nosepon  27605  nolesgn2ores  27612  nogesgn1ores  27614  nosepne  27620  nolt02o  27635  nosupbnd1lem5  27652  madebdaylemlrcut  27845  madebday  27846  sltlpss  27854  addsproplem2  27914  sleadd1  27933  addsuniflem  27945  mulsproplem9  28064  ssltmul1  28087  ssltmul2  28088  muls0ord  28125  precsexlem9  28154  precsexlem11  28156  recsex  28158  abssnid  28182  sltonold  28199  onnolt  28204  eucliddivs  28302  elnnzs  28326  expsne0  28360  zs12zodd  28393  zs12bday  28395  lmieu  28763  upgrpredgv  29118  edglnl  29122  eucrct2eupth  30223  frgrogt3nreg  30375  nvmul0or  30628  hvmul0or  31003  snsssng  32492  disjxpin  32566  expgt0b  32797  subfacp1lem4  35225  satfvsucsuc  35407  satfrnmapom  35412  sat1el2xp  35421  gonarlem  35436  gonar  35437  goalrlem  35438  goalr  35439  fmlasucdisj  35441  satffunlem1lem1  35444  satffunlem2lem1  35446  untsucf  35752  dfon2lem6  35828  broutsideof2  36162  btwnoutside  36165  broutsideof3  36166  outsideoftr  36169  lineunray  36187  lineelsb2  36188  finminlem  36358  nn0prpw  36363  refssfne  36398  meran1  36451  ontgval  36471  ordcmp  36487  bj-sngltag  37023  bj-prmoore  37155  topdifinfindis  37386  icoreclin  37397  rdgssun  37418  finxpsuclem  37437  poimirlem24  37690  poimirlem25  37691  poimirlem29  37695  poimirlem31  37697  mblfinlem2  37704  ovoliunnfl  37708  itg2addnclem  37717  sdclem2  37788  fdc  37791  divrngidl  38074  lkreqN  39215  cvrnbtwn4  39324  4atlem12  39657  elpaddn0  39845  paddasslem17  39881  paddidm  39886  pmapjoin  39897  llnexchb2  39914  dalawlem13  39928  dalawlem14  39929  dochkrshp4  41434  lcfl6  41545  lcmineqlem  42091  primrootspoweq0  42145  aks6d1c1  42155  sticksstones22  42207  aks6d1c6lem3  42211  oexpreposd  42361  expeqidd  42364  sn-remul0ord  42447  sn-sup2  42530  fphpdo  42856  pellfundex  42925  jm2.19lem4  43031  jm2.26a  43039  ordnexbtwnsuc  43306  onov0suclim  43313  oege2  43346  succlg  43367  dflim5  43368  oacl2g  43369  omcl2  43372  omcl3g  43373  naddgeoa  43433  safesnsupfiss  43454  fzunt  43494  fzuntd  43495  fzunt1d  43496  fzuntgd  43497  relexpmulg  43749  relexp01min  43752  relexpxpmin  43756  relexpaddss  43757  clsk1indlem3  44082  or2expropbi  47071  ich2exprop  47508  poprelb  47561  reuopreuprim  47563  goldbachthlem2  47583  requad01  47658  evenltle  47754  gbowge7  47800  bgoldbtbndlem3  47844  elclnbgrelnbgr  47862  clnbgrel  47865  dfclnbgr6  47893  dfnbgr6  47894  dfsclnbgr6  47895  upgrimpths  47946  clnbgrgrim  47971  isubgr3stgrlem4  48006  isubgr3stgrlem7  48009  grlimgredgex  48037  gpgedgvtx1  48099  gpgvtxedg0  48100  gpgvtxedg1  48101  lidldomn1  48268  uzlidlring  48272  prelrrx2b  48752  line2y  48793  itschlc0xyqsol1  48804  itsclc0xyqsolr  48807  inlinecirc02plem  48824