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  5370  relop  5793  poltletr  6081  ordnbtwn  6402  eqfnun  6971  oeoa  8515  oeoe  8517  ssnnfi  9083  domnsymfi  9114  unwdomg  9476  numwdom  9953  infpssrlem5  10201  fin23lem24  10216  fin23lem28  10234  fin1a2lem10  10303  zornn0g  10399  gchdomtri  10523  fpwwe2lem11  10535  fpwwe2lem12  10536  msqgt0  11640  recextlem2  11751  lemul1a  11978  nnne0  12162  nnnn0addcl  12414  un0addcl  12417  un0mulcl  12418  elz2  12489  mul2lt0bi  13001  xaddnemnf  13138  xaddnepnf  13139  rexmul  13173  xlemul1a  13190  xrsupsslem  13209  xrinfmsslem  13210  ixxun  13264  fzsplit2  13452  fzsuc2  13485  elfzp12  13506  seqf1olem2  13949  expp1  13975  expneg  13976  expcllem  13979  mulexpz  14009  expaddz  14013  expmulz  14015  zzlesq  14113  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd4  14204  bcpasc  14228  ccatass  14495  ccatrn  14496  ccatswrd  14575  ccatpfx  14607  cats1un  14627  revccat  14672  summo  15624  sumss2  15633  fsumsplit  15648  geomulcvg  15783  fprodsplit  15873  bpoly2  15964  bpoly3  15965  ef0lem  15985  odd2np1  16252  sadcaddlem  16368  gcdcllem3  16412  dvdslcm  16509  lcmeq0  16511  lcmcl  16512  lcmneg  16514  lcmgcd  16518  rpexp1i  16634  pcid  16785  4sqlem16  16872  funcres2c  17810  lubun  18421  mulgneg  18971  mulgnn0z  18980  frgpup3lem  19656  gsumzunsnd  19835  gsumunsnfd  19836  dprddisj2  19920  dmdprdsplit2  19927  dprdsplit  19929  gsumdixp  20204  lssvs0or  21017  evlslem4  21981  refun0  23400  txhaus  23532  xkoptsub  23539  ptunhmeo  23693  xpsxmetlem  24265  xpsmet  24268  mbfss  25545  itg1addlem2  25596  iblss2  25705  itgsplit  25735  limcres  25785  ftc1lem5  25945  coe1mul3  26002  dgrlt  26170  abelthlem3  26341  atanlogaddlem  26821  atanlogsub  26824  atans2  26839  efrlim  26877  efrlimOLD  26878  bposlem2  27194  lgsdir2lem4  27237  2sqb  27341  pntpbnd1  27495  ostthlem1  27536  nosepdm  27594  nosupbnd2lem1  27625  negsid  27952  elzn0s  28291  zsbday  28299  zscut  28300  expsp1  28321  hlbtwn  28556  cgracol  28773  inaghl  28790  brbtwn2  28850  axcontlem2  28910  ifnebib  32493  isoun  32644  eliccelico  32720  elicoelioo  32721  fzsplit3  32736  prodpr  32771  zarclsun  33837  xrge0iifhom  33904  esumsplit  34020  esumpad2  34023  sibfinima  34307  circlemethhgt  34611  bnj1137  34962  subfacp1lem4  35160  subfacp1lem5  35161  mclsax  35546  poimirlem2  37606  poimirlem8  37612  poimirlem22  37626  poimirlem28  37632  ftc1cnnc  37676  ftc1anclem2  37678  fdc  37729  incsequz2  37733  unichnidl  38015  lkrss2N  39152  cdlemg27b  40679  tendoex  40958  dihmeetlem2N  41282  dvh3dim3N  41432  aks6d1c2p2  42096  hashscontpow  42099  aks6d1c5  42116  sticksstones1  42123  sticksstones2  42124  unitscyglem2  42173  ofun  42213  sn-nnne0  42437  nn0addcom  42439  nn0mulcom  42443  zmulcomlem  42444  rexzrexnn0  42781  pell14qrexpcl  42844  elpell1qr2  42849  acongeq  42960  jm2.23  42973  rpnnen3  43009  mnringmulrcld  44205  mnuprdlem3  44251  radcnvrat  44291  sumpair  45017  cncfiooicclem1  45878  fourierdlem80  46171  fourierdlem93  46184  fullthinc  49439