Theorem jaodan 956

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

Syntax hints:   → wi 4   ∧ wa 396   ∨ wo 845

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 397  df-or 846

This theorem is referenced by:  mpjaodan  957  andi  1006  ccase  1036  mpjao3danOLD  1432  axpr  5425  relop  5848  poltletr  6130  ordnbtwn  6454  eqfnun  7035  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  19639  gsumzunsnd  19818  gsumunsnfd  19819  dprddisj2  19903  dmdprdsplit2  19910  dprdsplit  19912  gsumdixp  20124  lssvs0or  20715  evlslem4  21628  refun0  23010  txhaus  23142  xkoptsub  23149  ptunhmeo  23303  xpsxmetlem  23876  xpsmet  23879  mbfss  25154  itg1addlem2  25205  iblss2  25314  itgsplit  25344  limcres  25394  ftc1lem5  25548  coe1mul3  25608  dgrlt  25771  abelthlem3  25936  atanlogaddlem  26407  atanlogsub  26410  atans2  26425  efrlim  26463  bposlem2  26777  lgsdir2lem4  26820  2sqb  26924  pntpbnd1  27078  ostthlem1  27119  nosepdm  27176  nosupbnd2lem1  27207  negsid  27504  hlbtwn  27851  cgracol  28068  inaghl  28085  brbtwn2  28152  axcontlem2  28212  ifnebib  31768  isoun  31910  eliccelico  31975  elicoelioo  31976  fzsplit3  31992  prodpr  32019  zarclsun  32838  xrge0iifhom  32905  esumsplit  33039  esumpad2  33042  sibfinima  33326  circlemethhgt  33643  bnj1137  33994  subfacp1lem4  34162  subfacp1lem5  34163  mclsax  34548  poimirlem2  36478  poimirlem8  36484  poimirlem22  36498  poimirlem28  36504  ftc1cnnc  36548  ftc1anclem2  36550  fdc  36601  incsequz2  36605  unichnidl  36887  lkrss2N  38027  cdlemg27b  39555  tendoex  39834  dihmeetlem2N  40158  dvh3dim3N  40308  aks6d1c2p2  40945  sticksstones1  40950  sticksstones2  40951  metakunt9  40981  ofun  41055  sn-nnne0  41317  nn0addcom  41319  nn0mulcom  41323  zmulcomlem  41324  rexzrexnn0  41527  pell14qrexpcl  41590  elpell1qr2  41595  acongeq  41707  jm2.23  41720  rpnnen3  41756  mnringmulrcld  42972  mnuprdlem3  43018  radcnvrat  43058  sumpair  43704  cncfiooicclem1  44595  fourierdlem80  44888  fourierdlem93  44901  fullthinc  47619