Theorem jaod 860

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

Syntax hints:   → wi 4   ∨ wo 848

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 849

This theorem is referenced by:  mpjaod  861  orel2  891  pm2.621  899  pm2.63  943  jaao  957  jaodan  960  ecase3d  1035  dedlema  1046  dedlemb  1047  cad0  1620  psssstr  4063  eqoreldif  4644  opthpr  4809  prel12g  4822  opthprneg  4823  axpr  5374  sotric  5570  sotr2  5574  sotr3  5581  relop  5807  suctr  6413  trsucss  6415  ordelinel  6428  fununi  6575  fnprb  7164  soisoi  7284  ordunisuc2  7796  poxp  8080  soxp  8081  frrlem12  8249  frrlem13  8250  tfrlem11  8329  omordi  8503  om00  8512  odi  8516  omeulem2  8520  oewordi  8529  nnmordi  8569  omsmolem  8595  swoord2  8679  nneneq  9142  dffi3  9346  inf3lem6  9554  cantnfle  9592  cantnflem1  9610  cantnflem2  9611  ttrcltr  9637  r1sdom  9698  r1ord3g  9703  rankxplim3  9805  carddom2  9901  wdomnumr  9986  alephordi  9996  alephdom  10003  cardaleph  10011  djuinf  10111  cfsuc  10179  cfsmolem  10192  sornom  10199  fin23lem25  10246  fin1a2lem11  10332  fin1a2s  10336  zorn2lem7  10424  ttukeylem5  10435  alephval2  10495  fpwwe2lem12  10565  gch2  10598  gchaclem  10601  prub  10917  sqgt0sr  11029  1re  11144  lelttr  11235  ltletr  11237  letr  11239  mul0or  11789  prodgt0  12000  mulge0b  12024  squeeze0  12057  sup2  12110  un0addcl  12446  un0mulcl  12447  nn0sub  12463  elnnz  12510  zindd  12605  rpneg  12951  xrlttri  13065  xrlelttr  13082  xrltletr  13083  xrletr  13084  qextlt  13130  qextle  13131  xmullem2  13192  xlemul1a  13215  xrsupexmnf  13232  xrinfmexpnf  13233  supxrun  13243  prunioo  13409  difreicc  13412  iccsplit  13413  uzsplit  13524  fzm1  13535  expcl2lem  14008  expeq0  14027  expnegz  14031  expaddz  14041  expmulz  14043  sqlecan  14144  facdiv  14222  facwordi  14224  bcpasc  14256  resqrex  15185  absexpz  15240  caubnd  15294  summo  15652  zsum  15653  zprod  15872  rpnnen2lem12  16162  ordvdsmul  16239  nn0rppwr  16500  nn0expgcd  16503  dvdsprime  16626  2mulprm  16632  ge2nprmge4  16640  prmdvdsexpr  16656  prmfac1  16659  pythagtriplem2  16757  4sqlem11  16895  vdwlem6  16926  vdwlem9  16929  vdwlem13  16933  cshwshashlem3  17037  prmlem0  17045  pleval2  18270  pltletr  18276  plelttr  18277  tsrlemax  18521  smndex1mgm  18844  f1omvdco2  19389  psgnunilem2  19436  efgredlemc  19686  frgpuptinv  19712  lt6abl  19836  dmdprdsplit2lem  19988  domneq0  20653  drngmul0orOLD  20706  lvecvs0or  21075  baspartn  22910  0top  22939  indistopon  22957  restntr  23138  cnindis  23248  cmpfi  23364  filconn  23839  ufprim  23865  ufildr  23887  alexsubALTlem2  24004  alexsubALTlem3  24005  alexsubALTlem4  24006  ovolicc2lem3  25488  rolle  25962  dvivthlem1  25981  coeaddlem  26222  dgrco  26249  plymul0or  26256  aalioulem3  26310  cxpge0  26660  cxpmul2z  26668  cxpcn3lem  26725  scvxcvx  26964  sqf11  27117  ppiublem1  27181  lgsdir2lem2  27305  lgsqrlem2  27326  2sqnn0  27417  2sqnn  27418  nosepon  27645  nolesgn2ores  27652  nogesgn1ores  27654  nosepne  27660  nolt02o  27675  nosupbnd1lem5  27692  madebdaylemlrcut  27907  madebday  27908  ltslpss  27916  addsproplem2  27978  leadds1  27997  addsuniflem  28009  mulsproplem9  28132  sltmuls1  28155  sltmuls2  28156  muls0ord  28193  precsexlem9  28223  precsexlem11  28225  recsex  28227  abssnid  28251  ltonold  28269  onnolt  28274  eucliddivs  28384  elnnzs  28409  expsne0  28444  bdaypw2n0bndlem  28471  bdayfinbndlem1  28475  z12zsodd  28490  lmieu  28868  upgrpredgv  29224  edglnl  29228  eucrct2eupth  30332  frgrogt3nreg  30484  nvmul0or  30737  hvmul0or  31112  snsssng  32600  disjxpin  32674  expgt0b  32907  subfacp1lem4  35396  satfvsucsuc  35578  satfrnmapom  35583  sat1el2xp  35592  gonarlem  35607  gonar  35608  goalrlem  35609  goalr  35610  fmlasucdisj  35612  satffunlem1lem1  35615  satffunlem2lem1  35617  untsucf  35923  dfon2lem6  35999  broutsideof2  36335  btwnoutside  36338  broutsideof3  36339  outsideoftr  36342  lineunray  36360  lineelsb2  36361  finminlem  36531  nn0prpw  36536  refssfne  36571  meran1  36624  ontgval  36644  ordcmp  36660  bj-sngltag  37228  bj-axseprep  37319  bj-prmoore  37365  topdifinfindis  37598  icoreclin  37609  rdgssun  37630  finxpsuclem  37649  poimirlem24  37892  poimirlem25  37893  poimirlem29  37897  poimirlem31  37899  mblfinlem2  37906  ovoliunnfl  37910  itg2addnclem  37919  sdclem2  37990  fdc  37993  divrngidl  38276  lkreqN  39543  cvrnbtwn4  39652  4atlem12  39985  elpaddn0  40173  paddasslem17  40209  paddidm  40214  pmapjoin  40225  llnexchb2  40242  dalawlem13  40256  dalawlem14  40257  dochkrshp4  41762  lcfl6  41873  lcmineqlem  42419  primrootspoweq0  42473  aks6d1c1  42483  sticksstones22  42535  aks6d1c6lem3  42539  oexpreposd  42689  expeqidd  42692  sn-remul0ord  42775  sn-sup2  42858  fphpdo  43171  pellfundex  43240  jm2.19lem4  43346  jm2.26a  43354  ordnexbtwnsuc  43621  onov0suclim  43628  oege2  43661  succlg  43682  dflim5  43683  oacl2g  43684  omcl2  43687  omcl3g  43688  naddgeoa  43748  safesnsupfiss  43768  fzunt  43808  fzuntd  43809  fzunt1d  43810  fzuntgd  43811  relexpmulg  44063  relexp01min  44066  relexpxpmin  44070  relexpaddss  44071  clsk1indlem3  44396  or2expropbi  47391  ich2exprop  47828  poprelb  47881  reuopreuprim  47883  goldbachthlem2  47903  requad01  47978  evenltle  48074  gbowge7  48120  bgoldbtbndlem3  48164  elclnbgrelnbgr  48182  clnbgrel  48185  dfclnbgr6  48213  dfnbgr6  48214  dfsclnbgr6  48215  upgrimpths  48266  clnbgrgrim  48291  isubgr3stgrlem4  48326  isubgr3stgrlem7  48329  grlimgredgex  48357  gpgedgvtx1  48419  gpgvtxedg0  48420  gpgvtxedg1  48421  lidldomn1  48588  uzlidlring  48592  prelrrx2b  49071  line2y  49112  itschlc0xyqsol1  49123  itsclc0xyqsolr  49126  inlinecirc02plem  49143