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  5425  relop  5848  poltletr  6130  ordnbtwn  6454  eqfnun  7034  oeoa  8593  oeoe  8595  ssnnfi  9165  ssnnfiOLD  9166  domnsymfi  9199  phplem3OLD  9215  unwdomg  9575  numwdom  10050  infpssrlem5  10298  fin23lem24  10313  fin23lem28  10331  fin1a2lem10  10400  zornn0g  10496  gchdomtri  10620  fpwwe2lem11  10632  fpwwe2lem12  10633  msqgt0  11730  recextlem2  11841  lemul1a  12064  nnne0  12242  nnnn0addcl  12498  un0addcl  12501  un0mulcl  12502  elz2  12572  mul2lt0bi  13076  xaddnemnf  13211  xaddnepnf  13212  rexmul  13246  xlemul1a  13263  xrsupsslem  13282  xrinfmsslem  13283  ixxun  13336  fzsplit2  13522  fzsuc2  13555  elfzp12  13576  seqf1olem2  14004  expp1  14030  expneg  14031  expcllem  14034  mulexpz  14064  expaddz  14068  expmulz  14070  zzlesq  14166  faclbnd4lem3  14251  faclbnd4lem4  14252  faclbnd4  14253  bcpasc  14277  ccatass  14534  ccatrn  14535  ccatswrd  14614  ccatpfx  14647  cats1un  14667  revccat  14712  summo  15659  sumss2  15668  fsumsplit  15683  geomulcvg  15818  fprodsplit  15906  bpoly2  15997  bpoly3  15998  ef0lem  16018  odd2np1  16280  sadcaddlem  16394  gcdcllem3  16438  dvdslcm  16531  lcmeq0  16533  lcmcl  16534  lcmneg  16536  lcmgcd  16540  rpexp1i  16656  pcid  16802  4sqlem16  16889  funcres2c  17848  lubun  18464  mulgneg  18966  mulgnn0z  18975  frgpup3lem  19638  gsumzunsnd  19816  gsumunsnfd  19817  dprddisj2  19901  dmdprdsplit2  19908  dprdsplit  19910  gsumdixp  20121  lssvs0or  20711  evlslem4  21619  refun0  23001  txhaus  23133  xkoptsub  23140  ptunhmeo  23294  xpsxmetlem  23867  xpsmet  23870  mbfss  25145  itg1addlem2  25196  iblss2  25305  itgsplit  25335  limcres  25385  ftc1lem5  25539  coe1mul3  25599  dgrlt  25762  abelthlem3  25927  atanlogaddlem  26398  atanlogsub  26401  atans2  26416  efrlim  26454  bposlem2  26768  lgsdir2lem4  26811  2sqb  26915  pntpbnd1  27069  ostthlem1  27110  nosepdm  27167  nosupbnd2lem1  27198  negsid  27495  hlbtwn  27842  cgracol  28059  inaghl  28076  brbtwn2  28143  axcontlem2  28203  ifnebib  31759  isoun  31901  eliccelico  31966  elicoelioo  31967  fzsplit3  31983  prodpr  32010  zarclsun  32788  xrge0iifhom  32855  esumsplit  32989  esumpad2  32992  sibfinima  33276  circlemethhgt  33593  bnj1137  33944  subfacp1lem4  34112  subfacp1lem5  34113  mclsax  34498  poimirlem2  36428  poimirlem8  36434  poimirlem22  36448  poimirlem28  36454  ftc1cnnc  36498  ftc1anclem2  36500  fdc  36551  incsequz2  36555  unichnidl  36837  lkrss2N  37977  cdlemg27b  39505  tendoex  39784  dihmeetlem2N  40108  dvh3dim3N  40258  aks6d1c2p2  40895  sticksstones1  40900  sticksstones2  40901  metakunt9  40931  ofun  41007  sn-nnne0  41265  nn0addcom  41267  nn0mulcom  41271  zmulcomlem  41272  rexzrexnn0  41475  pell14qrexpcl  41538  elpell1qr2  41543  acongeq  41655  jm2.23  41668  rpnnen3  41704  mnringmulrcld  42920  mnuprdlem3  42966  radcnvrat  43006  sumpair  43652  cncfiooicclem1  44544  fourierdlem80  44837  fourierdlem93  44850  fullthinc  47568