Theorem jaodan 959

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 412	. . 3 ⊢ (𝜑 → (𝜓 → 𝜒))
3		jaodan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
4	3	ex 412	. . 3 ⊢ (𝜑 → (𝜃 → 𝜒))
5	2, 4	jaod 859	. 2 ⊢ (𝜑 → ((𝜓 ∨ 𝜃) → 𝜒))
6	5	imp 406	1 ⊢ ((𝜑 ∧ (𝜓 ∨ 𝜃)) → 𝜒)

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

This theorem is referenced by:  mpjaodan  960  andi  1009  ccase  1037  axprOLD  5374  relop  5797  poltletr  6087  ordnbtwn  6410  eqfnun  6980  oeoa  8523  oeoe  8525  ssnnfi  9092  domnsymfi  9122  unwdomg  9487  numwdom  9967  infpssrlem5  10215  fin23lem24  10230  fin23lem28  10248  fin1a2lem10  10317  zornn0g  10413  gchdomtri  10538  fpwwe2lem11  10550  fpwwe2lem12  10551  msqgt0  11655  recextlem2  11766  lemul1a  11993  nnne0  12177  nnnn0addcl  12429  un0addcl  12432  un0mulcl  12433  elz2  12504  mul2lt0bi  13011  xaddnemnf  13149  xaddnepnf  13150  rexmul  13184  xlemul1a  13201  xrsupsslem  13220  xrinfmsslem  13221  ixxun  13275  fzsplit2  13463  fzsuc2  13496  elfzp12  13517  seqf1olem2  13963  expp1  13989  expneg  13990  expcllem  13993  mulexpz  14023  expaddz  14027  expmulz  14029  zzlesq  14127  faclbnd4lem3  14216  faclbnd4lem4  14217  faclbnd4  14218  bcpasc  14242  ccatass  14510  ccatrn  14511  ccatswrd  14590  ccatpfx  14622  cats1un  14642  revccat  14687  summo  15638  sumss2  15647  fsumsplit  15662  geomulcvg  15797  fprodsplit  15887  bpoly2  15978  bpoly3  15979  ef0lem  15999  odd2np1  16266  sadcaddlem  16382  gcdcllem3  16426  dvdslcm  16523  lcmeq0  16525  lcmcl  16526  lcmneg  16528  lcmgcd  16532  rpexp1i  16648  pcid  16799  4sqlem16  16886  funcres2c  17825  lubun  18436  mulgneg  19020  mulgnn0z  19029  frgpup3lem  19704  gsumzunsnd  19883  gsumunsnfd  19884  dprddisj2  19968  dmdprdsplit2  19975  dprdsplit  19977  gsumdixp  20252  lssvs0or  21063  evlslem4  22029  refun0  23457  txhaus  23589  xkoptsub  23596  ptunhmeo  23750  xpsxmetlem  24321  xpsmet  24324  mbfss  25601  itg1addlem2  25652  iblss2  25761  itgsplit  25791  limcres  25841  ftc1lem5  26001  coe1mul3  26058  dgrlt  26226  abelthlem3  26397  atanlogaddlem  26877  atanlogsub  26880  atans2  26895  efrlim  26933  efrlimOLD  26934  bposlem2  27250  lgsdir2lem4  27293  2sqb  27397  pntpbnd1  27551  ostthlem1  27592  nosepdm  27650  nosupbnd2lem1  27681  negsid  28010  elzn0s  28356  zsbday  28364  zscut  28365  expsp1  28387  hlbtwn  28632  cgracol  28849  inaghl  28866  brbtwn2  28927  axcontlem2  28987  ifnebib  32573  isoun  32730  eliccelico  32806  elicoelioo  32807  fzsplit3  32822  prodpr  32856  zarclsun  33976  xrge0iifhom  34043  esumsplit  34159  esumpad2  34162  sibfinima  34445  circlemethhgt  34749  bnj1137  35100  subfacp1lem4  35326  subfacp1lem5  35327  mclsax  35712  poimirlem2  37762  poimirlem8  37768  poimirlem22  37782  poimirlem28  37788  ftc1cnnc  37832  ftc1anclem2  37834  fdc  37885  incsequz2  37889  unichnidl  38171  lkrss2N  39368  cdlemg27b  40895  tendoex  41174  dihmeetlem2N  41498  dvh3dim3N  41648  aks6d1c2p2  42312  hashscontpow  42315  aks6d1c5  42332  sticksstones1  42339  sticksstones2  42340  unitscyglem2  42389  ofun  42434  sn-nnne0  42657  nn0addcom  42659  nn0mulcom  42663  zmulcomlem  42664  rexzrexnn0  42988  pell14qrexpcl  43051  elpell1qr2  43056  acongeq  43167  jm2.23  43180  rpnnen3  43216  mnringmulrcld  44411  mnuprdlem3  44457  radcnvrat  44497  sumpair  45222  cncfiooicclem1  46079  fourierdlem80  46372  fourierdlem93  46385  fullthinc  49637