Theorem jaodan 958

Description: Deduction disjoining the antecedents of two implications. (Contributed by NM, 14-Oct-2005.)

Hypotheses

Ref	Expression
jaodan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
jaodan.2	⊢ ((𝜑 ∧ 𝜃) → 𝜒)

Assertion

Ref	Expression
jaodan	⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Proof of Theorem jaodan

Step	Hyp	Ref	Expression
1		jaodan.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	ex 416	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 416	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 859	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 410	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 399   ∨ 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 210  df-an 400  df-or 848

This theorem is referenced by:  mpjaodan  959  andi  1008  ccase  1038  mpjao3danOLD  1434  axpr  5321  relop  5719  poltletr  5997  ordnbtwn  6303  oeoa  8325  oeoe  8327  phplem3  8827  ssnnfi  8847  ssnnfiOLD  8848  unwdomg  9200  numwdom  9673  infpssrlem5  9921  fin23lem24  9936  fin23lem28  9954  fin1a2lem10  10023  zornn0g  10119  gchdomtri  10243  fpwwe2lem11  10255  fpwwe2lem12  10256  msqgt0  11352  recextlem2  11463  lemul1a  11686  nnnn0addcl  12120  un0addcl  12123  un0mulcl  12124  elz2  12194  mul2lt0bi  12692  xaddnemnf  12826  xaddnepnf  12827  rexmul  12861  xlemul1a  12878  xrsupsslem  12897  xrinfmsslem  12898  ixxun  12951  fzsplit2  13137  fzsuc2  13170  elfzp12  13191  seqf1olem2  13616  expp1  13642  expneg  13643  expcllem  13646  mulexpz  13675  expaddz  13679  expmulz  13681  faclbnd4lem3  13861  faclbnd4lem4  13862  faclbnd4  13863  bcpasc  13887  ccatass  14145  ccatrn  14146  ccatswrd  14233  ccatpfx  14266  cats1un  14286  revccat  14331  summo  15281  sumss2  15290  fsumsplit  15305  geomulcvg  15440  fprodsplit  15528  bpoly2  15619  bpoly3  15620  ef0lem  15640  odd2np1  15902  sadcaddlem  16016  gcdcllem3  16060  dvdslcm  16155  lcmeq0  16157  lcmcl  16158  lcmneg  16160  lcmgcd  16164  rpexp1i  16280  pcid  16426  4sqlem16  16513  funcres2c  17408  lubun  18021  mulgneg  18510  mulgnn0z  18518  frgpup3lem  19167  gsumzunsnd  19341  gsumunsnfd  19342  dprddisj2  19426  dmdprdsplit2  19433  dprdsplit  19435  gsumdixp  19627  lssvs0or  20147  evlslem4  21034  refun0  22412  txhaus  22544  xkoptsub  22551  ptunhmeo  22705  xpsxmetlem  23277  xpsmet  23280  mbfss  24543  itg1addlem2  24594  iblss2  24703  itgsplit  24733  limcres  24783  ftc1lem5  24937  coe1mul3  24997  dgrlt  25160  abelthlem3  25325  atanlogaddlem  25796  atanlogsub  25799  atans2  25814  efrlim  25852  bposlem2  26166  lgsdir2lem4  26209  2sqb  26313  pntpbnd1  26467  ostthlem1  26508  hlbtwn  26702  cgracol  26919  inaghl  26936  brbtwn2  26996  axcontlem2  27056  isoun  30754  eliccelico  30818  elicoelioo  30819  fzsplit3  30835  prodpr  30860  zarclsun  31534  xrge0iifhom  31601  esumsplit  31733  esumpad2  31736  sibfinima  32018  circlemethhgt  32335  bnj1137  32688  subfacp1lem4  32858  subfacp1lem5  32859  mclsax  33244  nosepdm  33624  nosupbnd2lem1  33655  poimirlem2  35516  poimirlem8  35522  poimirlem22  35536  poimirlem28  35542  ftc1cnnc  35586  ftc1anclem2  35588  eqfnun  35617  fdc  35640  incsequz2  35644  unichnidl  35926  lkrss2N  36920  cdlemg27b  38447  tendoex  38726  dihmeetlem2N  39050  dvh3dim3N  39200  sticksstones1  39824  sticksstones2  39825  metakunt9  39855  ofun  39924  rexzrexnn0  40329  pell14qrexpcl  40392  elpell1qr2  40397  acongeq  40508  jm2.23  40521  rpnnen3  40557  mnringmulrcld  41519  mnuprdlem3  41565  radcnvrat  41605  sumpair  42251  cncfiooicclem1  43109  fourierdlem80  43402  fourierdlem93  43415  fullthinc  46000