Theorem jaodan 957

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

Syntax hints:   → wi 4   ∧ wa 397   ∨ wo 846

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 206  df-an 398  df-or 847

This theorem is referenced by:  mpjaodan  958  andi  1007  ccase  1037  mpjao3danOLD  1433  axpr  5427  relop  5851  poltletr  6134  ordnbtwn  6458  eqfnun  7039  oeoa  8597  oeoe  8599  ssnnfi  9169  ssnnfiOLD  9170  domnsymfi  9203  phplem3OLD  9219  unwdomg  9579  numwdom  10054  infpssrlem5  10302  fin23lem24  10317  fin23lem28  10335  fin1a2lem10  10404  zornn0g  10500  gchdomtri  10624  fpwwe2lem11  10636  fpwwe2lem12  10637  msqgt0  11734  recextlem2  11845  lemul1a  12068  nnne0  12246  nnnn0addcl  12502  un0addcl  12505  un0mulcl  12506  elz2  12576  mul2lt0bi  13080  xaddnemnf  13215  xaddnepnf  13216  rexmul  13250  xlemul1a  13267  xrsupsslem  13286  xrinfmsslem  13287  ixxun  13340  fzsplit2  13526  fzsuc2  13559  elfzp12  13580  seqf1olem2  14008  expp1  14034  expneg  14035  expcllem  14038  mulexpz  14068  expaddz  14072  expmulz  14074  zzlesq  14170  faclbnd4lem3  14255  faclbnd4lem4  14256  faclbnd4  14257  bcpasc  14281  ccatass  14538  ccatrn  14539  ccatswrd  14618  ccatpfx  14651  cats1un  14671  revccat  14716  summo  15663  sumss2  15672  fsumsplit  15687  geomulcvg  15822  fprodsplit  15910  bpoly2  16001  bpoly3  16002  ef0lem  16022  odd2np1  16284  sadcaddlem  16398  gcdcllem3  16442  dvdslcm  16535  lcmeq0  16537  lcmcl  16538  lcmneg  16540  lcmgcd  16544  rpexp1i  16660  pcid  16806  4sqlem16  16893  funcres2c  17852  lubun  18468  mulgneg  18972  mulgnn0z  18981  frgpup3lem  19645  gsumzunsnd  19824  gsumunsnfd  19825  dprddisj2  19909  dmdprdsplit2  19916  dprdsplit  19918  gsumdixp  20131  lssvs0or  20723  evlslem4  21637  refun0  23019  txhaus  23151  xkoptsub  23158  ptunhmeo  23312  xpsxmetlem  23885  xpsmet  23888  mbfss  25163  itg1addlem2  25214  iblss2  25323  itgsplit  25353  limcres  25403  ftc1lem5  25557  coe1mul3  25617  dgrlt  25780  abelthlem3  25945  atanlogaddlem  26418  atanlogsub  26421  atans2  26436  efrlim  26474  bposlem2  26788  lgsdir2lem4  26831  2sqb  26935  pntpbnd1  27089  ostthlem1  27130  nosepdm  27187  nosupbnd2lem1  27218  negsid  27515  hlbtwn  27862  cgracol  28079  inaghl  28096  brbtwn2  28163  axcontlem2  28223  ifnebib  31781  isoun  31923  eliccelico  31988  elicoelioo  31989  fzsplit3  32005  prodpr  32032  zarclsun  32850  xrge0iifhom  32917  esumsplit  33051  esumpad2  33054  sibfinima  33338  circlemethhgt  33655  bnj1137  34006  subfacp1lem4  34174  subfacp1lem5  34175  mclsax  34560  poimirlem2  36490  poimirlem8  36496  poimirlem22  36510  poimirlem28  36516  ftc1cnnc  36560  ftc1anclem2  36562  fdc  36613  incsequz2  36617  unichnidl  36899  lkrss2N  38039  cdlemg27b  39567  tendoex  39846  dihmeetlem2N  40170  dvh3dim3N  40320  aks6d1c2p2  40957  sticksstones1  40962  sticksstones2  40963  metakunt9  40993  ofun  41058  sn-nnne0  41321  nn0addcom  41323  nn0mulcom  41327  zmulcomlem  41328  rexzrexnn0  41542  pell14qrexpcl  41605  elpell1qr2  41610  acongeq  41722  jm2.23  41735  rpnnen3  41771  mnringmulrcld  42987  mnuprdlem3  43033  radcnvrat  43073  sumpair  43719  cncfiooicclem1  44609  fourierdlem80  44902  fourierdlem93  44915  fullthinc  47666