Theorem jaodan 822

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

Syntax hints:   → wi 4   ∨ wo 382   ∧ wa 383

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 196  df-or 384  df-an 385

This theorem is referenced by:  mpjaodan  823  andi  907  ccase  984  mpjao3dan  1387  relop  5194  poltletr  5447  ordnbtwn  5733  oeoa  7564  oeoe  7566  phplem3  8026  ssnnfi  8064  unwdomg  8372  numwdom  8765  infpssrlem5  9012  fin23lem24  9027  fin23lem28  9045  fin1a2lem10  9114  zornn0g  9210  gchdomtri  9330  fpwwe2lem12  9342  fpwwe2lem13  9343  msqgt0  10427  recextlem2  10537  lemul1a  10756  nnnn0addcl  11200  un0addcl  11203  un0mulcl  11204  elz2  11271  mul2lt0bi  11812  xaddnemnf  11941  xaddnepnf  11942  rexmul  11973  xlemul1a  11990  xrsupsslem  12009  xrinfmsslem  12010  ixxun  12062  fzsplit2  12237  fzsuc2  12268  elfzp12  12288  seqf1olem2  12703  expp1  12729  expneg  12730  expcllem  12733  mulexpz  12762  expaddz  12766  expmulz  12768  faclbnd4lem3  12944  faclbnd4lem4  12945  faclbnd4  12946  bcpasc  12970  ccatass  13224  ccatrn  13225  ccatswrd  13308  cats1un  13327  revccat  13366  summo  14295  sumss2  14304  fsumsplit  14318  geomulcvg  14446  fprodsplit  14535  bpoly2  14627  bpoly3  14628  ef0lem  14648  odd2np1  14903  sadcaddlem  15017  gcdcllem3  15061  dvdslcm  15149  lcmeq0  15151  lcmcl  15152  lcmneg  15154  lcmgcd  15158  rpexp1i  15271  pcid  15415  4sqlem16  15502  funcres2c  16384  lubun  16946  mulgneg  17383  mulgnn0z  17390  frgpup3lem  18013  gsumzunsnd  18178  gsumunsnfd  18179  dprddisj2  18261  dmdprdsplit2  18268  dprdsplit  18270  gsumdixp  18432  lssvs0or  18931  evlslem4  19329  refun0  21128  txhaus  21260  xkoptsub  21267  ptunhmeo  21421  xpsxmetlem  21994  xpsmet  21997  mbfss  23219  itg1addlem2  23270  iblss2  23378  itgsplit  23408  limcres  23456  ftc1lem5  23607  coe1mul3  23663  dgrlt  23826  abelthlem3  23991  atanlogaddlem  24440  atanlogsub  24443  atans2  24458  efrlim  24496  bposlem2  24810  lgsdir2lem4  24853  2sqb  24957  pntpbnd1  25075  ostthlem1  25116  hlbtwn  25306  cgracol  25519  inaghl  25531  brbtwn2  25585  axcontlem2  25645  uvtx01vtx  26020  isoun  28862  nn0sqeq1  28901  eliccelico  28929  elicoelioo  28930  fzsplit3  28940  xrge0iifhom  29311  esumsplit  29442  esumpad2  29445  sibfinima  29728  bnj1137  30317  subfacp1lem4  30419  subfacp1lem5  30420  mclsax  30720  poimirlem2  32581  poimirlem8  32587  poimirlem22  32601  poimirlem28  32607  ftc1cnnc  32654  ftc1anclem2  32656  eqfnun  32686  fdc  32711  incsequz2  32715  unichnidl  33000  lkrss2N  33474  cdlemg27b  35002  tendoex  35281  dihmeetlem2N  35606  dvh3dim3N  35756  rexzrexnn0  36386  pell14qrexpcl  36449  elpell1qr2  36454  acongeq  36568  jm2.23  36581  rpnnen3  36617  radcnvrat  37535  sumpair  38217  cncfiooicclem1  38779  fourierdlem80  39079  fourierdlem93  39092  ccatpfx  40272