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  5381  relop  5804  poltletr  6093  ordnbtwn  6415  eqfnun  6991  oeoa  8538  oeoe  8540  ssnnfi  9110  domnsymfi  9141  unwdomg  9513  numwdom  9988  infpssrlem5  10236  fin23lem24  10251  fin23lem28  10269  fin1a2lem10  10338  zornn0g  10434  gchdomtri  10558  fpwwe2lem11  10570  fpwwe2lem12  10571  msqgt0  11674  recextlem2  11785  lemul1a  12012  nnne0  12196  nnnn0addcl  12448  un0addcl  12451  un0mulcl  12452  elz2  12523  mul2lt0bi  13035  xaddnemnf  13172  xaddnepnf  13173  rexmul  13207  xlemul1a  13224  xrsupsslem  13243  xrinfmsslem  13244  ixxun  13298  fzsplit2  13486  fzsuc2  13519  elfzp12  13540  seqf1olem2  13983  expp1  14009  expneg  14010  expcllem  14013  mulexpz  14043  expaddz  14047  expmulz  14049  zzlesq  14147  faclbnd4lem3  14236  faclbnd4lem4  14237  faclbnd4  14238  bcpasc  14262  ccatass  14529  ccatrn  14530  ccatswrd  14609  ccatpfx  14642  cats1un  14662  revccat  14707  summo  15659  sumss2  15668  fsumsplit  15683  geomulcvg  15818  fprodsplit  15908  bpoly2  15999  bpoly3  16000  ef0lem  16020  odd2np1  16287  sadcaddlem  16403  gcdcllem3  16447  dvdslcm  16544  lcmeq0  16546  lcmcl  16547  lcmneg  16549  lcmgcd  16553  rpexp1i  16669  pcid  16820  4sqlem16  16907  funcres2c  17845  lubun  18456  mulgneg  19006  mulgnn0z  19015  frgpup3lem  19691  gsumzunsnd  19870  gsumunsnfd  19871  dprddisj2  19955  dmdprdsplit2  19962  dprdsplit  19964  gsumdixp  20239  lssvs0or  21052  evlslem4  22016  refun0  23435  txhaus  23567  xkoptsub  23574  ptunhmeo  23728  xpsxmetlem  24300  xpsmet  24303  mbfss  25580  itg1addlem2  25631  iblss2  25740  itgsplit  25770  limcres  25820  ftc1lem5  25980  coe1mul3  26037  dgrlt  26205  abelthlem3  26376  atanlogaddlem  26856  atanlogsub  26859  atans2  26874  efrlim  26912  efrlimOLD  26913  bposlem2  27229  lgsdir2lem4  27272  2sqb  27376  pntpbnd1  27530  ostthlem1  27571  nosepdm  27629  nosupbnd2lem1  27660  negsid  27987  elzn0s  28326  zsbday  28334  zscut  28335  expsp1  28356  hlbtwn  28591  cgracol  28808  inaghl  28825  brbtwn2  28885  axcontlem2  28945  ifnebib  32528  isoun  32675  eliccelico  32750  elicoelioo  32751  fzsplit3  32766  prodpr  32801  zarclsun  33853  xrge0iifhom  33920  esumsplit  34036  esumpad2  34039  sibfinima  34323  circlemethhgt  34627  bnj1137  34978  subfacp1lem4  35163  subfacp1lem5  35164  mclsax  35549  poimirlem2  37609  poimirlem8  37615  poimirlem22  37629  poimirlem28  37635  ftc1cnnc  37679  ftc1anclem2  37681  fdc  37732  incsequz2  37736  unichnidl  38018  lkrss2N  39155  cdlemg27b  40683  tendoex  40962  dihmeetlem2N  41286  dvh3dim3N  41436  aks6d1c2p2  42100  hashscontpow  42103  aks6d1c5  42120  sticksstones1  42127  sticksstones2  42128  unitscyglem2  42177  ofun  42217  sn-nnne0  42441  nn0addcom  42443  nn0mulcom  42447  zmulcomlem  42448  rexzrexnn0  42785  pell14qrexpcl  42848  elpell1qr2  42853  acongeq  42965  jm2.23  42978  rpnnen3  43014  mnringmulrcld  44210  mnuprdlem3  44256  radcnvrat  44296  sumpair  45022  cncfiooicclem1  45884  fourierdlem80  46177  fourierdlem93  46190  fullthinc  49432