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  4068  eqoreldif  4645  opthpr  4811  prel12g  4824  opthprneg  4825  axpr  5377  sotric  5569  sotr2  5573  sotr3  5580  relop  5804  suctr  6408  trsucss  6410  ordelinel  6423  fununi  6575  fnprb  7164  soisoi  7285  ordunisuc2  7800  poxp  8084  soxp  8085  frrlem12  8253  frrlem13  8254  tfrlem11  8333  omordi  8507  om00  8516  odi  8520  omeulem2  8524  oewordi  8532  nnmordi  8572  omsmolem  8598  swoord2  8681  nneneq  9147  dffi3  9358  inf3lem6  9562  cantnfle  9600  cantnflem1  9618  cantnflem2  9619  ttrcltr  9645  r1sdom  9703  r1ord3g  9708  rankxplim3  9810  carddom2  9906  wdomnumr  9993  alephordi  10003  alephdom  10010  cardaleph  10018  djuinf  10118  cfsuc  10186  cfsmolem  10199  sornom  10206  fin23lem25  10253  fin1a2lem11  10339  fin1a2s  10343  zorn2lem7  10431  ttukeylem5  10442  alephval2  10501  fpwwe2lem12  10571  gch2  10604  gchaclem  10607  prub  10923  sqgt0sr  11035  1re  11150  lelttr  11240  ltletr  11242  letr  11244  mul0or  11794  prodgt0  12005  mulge0b  12029  squeeze0  12062  sup2  12115  un0addcl  12451  un0mulcl  12452  nn0sub  12468  elnnz  12515  zindd  12611  rpneg  12961  xrlttri  13075  xrlelttr  13092  xrltletr  13093  xrletr  13094  qextlt  13139  qextle  13140  xmullem2  13201  xlemul1a  13224  xrsupexmnf  13241  xrinfmexpnf  13242  supxrun  13252  prunioo  13418  difreicc  13421  iccsplit  13422  uzsplit  13533  fzm1  13544  expcl2lem  14014  expeq0  14033  expnegz  14037  expaddz  14047  expmulz  14049  sqlecan  14150  facdiv  14228  facwordi  14230  bcpasc  14262  resqrex  15192  absexpz  15247  caubnd  15301  summo  15659  zsum  15660  zprod  15879  rpnnen2lem12  16169  ordvdsmul  16246  nn0rppwr  16507  nn0expgcd  16510  dvdsprime  16633  2mulprm  16639  ge2nprmge4  16647  prmdvdsexpr  16663  prmfac1  16666  pythagtriplem2  16764  4sqlem11  16902  vdwlem6  16933  vdwlem9  16936  vdwlem13  16940  cshwshashlem3  17044  prmlem0  17052  pleval2  18272  pltletr  18278  plelttr  18279  tsrlemax  18521  smndex1mgm  18810  f1omvdco2  19354  psgnunilem2  19401  efgredlemc  19651  frgpuptinv  19677  lt6abl  19801  dmdprdsplit2lem  19953  domneq0  20593  drngmul0orOLD  20646  lvecvs0or  20994  baspartn  22817  0top  22846  indistopon  22864  restntr  23045  cnindis  23155  cmpfi  23271  filconn  23746  ufprim  23772  ufildr  23794  alexsubALTlem2  23911  alexsubALTlem3  23912  alexsubALTlem4  23913  ovolicc2lem3  25396  rolle  25870  dvivthlem1  25889  coeaddlem  26130  dgrco  26157  plymul0or  26164  aalioulem3  26218  cxpge0  26568  cxpmul2z  26576  cxpcn3lem  26633  scvxcvx  26872  sqf11  27025  ppiublem1  27089  lgsdir2lem2  27213  lgsqrlem2  27234  2sqnn0  27325  2sqnn  27326  nosepon  27553  nolesgn2ores  27560  nogesgn1ores  27562  nosepne  27568  nolt02o  27583  nosupbnd1lem5  27600  madebdaylemlrcut  27786  madebday  27787  sltlpss  27795  addsproplem2  27853  sleadd1  27872  addsuniflem  27884  mulsproplem9  28003  ssltmul1  28026  ssltmul2  28027  muls0ord  28064  precsexlem9  28093  precsexlem11  28095  recsex  28097  abssnid  28121  sltonold  28138  onnolt  28143  eucliddivs  28241  elnnzs  28265  expsne0  28297  zs12bday  28319  lmieu  28687  upgrpredgv  29042  edglnl  29046  eucrct2eupth  30147  frgrogt3nreg  30299  nvmul0or  30552  hvmul0or  30927  snsssng  32416  disjxpin  32490  expgt0b  32714  subfacp1lem4  35143  satfvsucsuc  35325  satfrnmapom  35330  sat1el2xp  35339  gonarlem  35354  gonar  35355  goalrlem  35356  goalr  35357  fmlasucdisj  35359  satffunlem1lem1  35362  satffunlem2lem1  35364  untsucf  35670  dfon2lem6  35749  broutsideof2  36083  btwnoutside  36086  broutsideof3  36087  outsideoftr  36090  lineunray  36108  lineelsb2  36109  finminlem  36279  nn0prpw  36284  refssfne  36319  meran1  36372  ontgval  36392  ordcmp  36408  bj-sngltag  36944  bj-prmoore  37076  topdifinfindis  37307  icoreclin  37318  rdgssun  37339  finxpsuclem  37358  poimirlem24  37611  poimirlem25  37612  poimirlem29  37616  poimirlem31  37618  mblfinlem2  37625  ovoliunnfl  37629  itg2addnclem  37638  sdclem2  37709  fdc  37712  divrngidl  37995  lkreqN  39136  cvrnbtwn4  39245  4atlem12  39579  elpaddn0  39767  paddasslem17  39803  paddidm  39808  pmapjoin  39819  llnexchb2  39836  dalawlem13  39850  dalawlem14  39851  dochkrshp4  41356  lcfl6  41467  lcmineqlem  42013  primrootspoweq0  42067  aks6d1c1  42077  sticksstones22  42129  aks6d1c6lem3  42133  oexpreposd  42283  expeqidd  42286  sn-remul0ord  42369  sn-sup2  42452  fphpdo  42778  pellfundex  42847  jm2.19lem4  42954  jm2.26a  42962  ordnexbtwnsuc  43229  onov0suclim  43236  oege2  43269  succlg  43290  dflim5  43291  oacl2g  43292  omcl2  43295  omcl3g  43296  naddgeoa  43356  safesnsupfiss  43377  fzunt  43417  fzuntd  43418  fzunt1d  43419  fzuntgd  43420  relexpmulg  43672  relexp01min  43675  relexpxpmin  43679  relexpaddss  43680  clsk1indlem3  44005  or2expropbi  47008  ich2exprop  47445  poprelb  47498  reuopreuprim  47500  goldbachthlem2  47520  requad01  47595  evenltle  47691  gbowge7  47737  bgoldbtbndlem3  47781  elclnbgrelnbgr  47799  clnbgrel  47802  dfclnbgr6  47829  dfnbgr6  47830  dfsclnbgr6  47831  upgrimpths  47882  clnbgrgrim  47907  isubgr3stgrlem4  47941  isubgr3stgrlem7  47944  gpgedgvtx1  48026  gpgvtxedg0  48027  gpgvtxedg1  48028  lidldomn1  48192  uzlidlring  48196  prelrrx2b  48676  line2y  48717  itschlc0xyqsol1  48728  itsclc0xyqsolr  48731  inlinecirc02plem  48748