Theorem jaodan 954

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

Syntax hints:   → wi 4   ∧ wa 398   ∨ wo 843

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 209  df-an 399  df-or 844

This theorem is referenced by:  mpjaodan  955  andi  1004  ccase  1032  mpjao3danOLD  1428  axpr  5331  relop  5723  poltletr  5994  ordnbtwn  6283  oeoa  8225  oeoe  8227  phplem3  8700  ssnnfi  8739  unwdomg  9050  numwdom  9487  infpssrlem5  9731  fin23lem24  9746  fin23lem28  9764  fin1a2lem10  9833  zornn0g  9929  gchdomtri  10053  fpwwe2lem12  10065  fpwwe2lem13  10066  msqgt0  11162  recextlem2  11273  lemul1a  11496  nnnn0addcl  11930  un0addcl  11933  un0mulcl  11934  elz2  12002  mul2lt0bi  12498  xaddnemnf  12632  xaddnepnf  12633  rexmul  12667  xlemul1a  12684  xrsupsslem  12703  xrinfmsslem  12704  ixxun  12757  fzsplit2  12935  fzsuc2  12968  elfzp12  12989  seqf1olem2  13413  expp1  13439  expneg  13440  expcllem  13443  mulexpz  13472  expaddz  13476  expmulz  13478  faclbnd4lem3  13658  faclbnd4lem4  13659  faclbnd4  13660  bcpasc  13684  ccatass  13944  ccatrn  13945  ccatswrd  14032  ccatpfx  14065  cats1un  14085  revccat  14130  summo  15076  sumss2  15085  fsumsplit  15099  geomulcvg  15234  fprodsplit  15322  bpoly2  15413  bpoly3  15414  ef0lem  15434  odd2np1  15692  sadcaddlem  15808  gcdcllem3  15852  dvdslcm  15944  lcmeq0  15946  lcmcl  15947  lcmneg  15949  lcmgcd  15953  rpexp1i  16067  pcid  16211  4sqlem16  16298  funcres2c  17173  lubun  17735  mulgneg  18248  mulgnn0z  18256  frgpup3lem  18905  gsumzunsnd  19078  gsumunsnfd  19079  dprddisj2  19163  dmdprdsplit2  19170  dprdsplit  19172  gsumdixp  19361  lssvs0or  19884  evlslem4  20290  refun0  22125  txhaus  22257  xkoptsub  22264  ptunhmeo  22418  xpsxmetlem  22991  xpsmet  22994  mbfss  24249  itg1addlem2  24300  iblss2  24408  itgsplit  24438  limcres  24486  ftc1lem5  24639  coe1mul3  24695  dgrlt  24858  abelthlem3  25023  atanlogaddlem  25493  atanlogsub  25496  atans2  25511  efrlim  25549  bposlem2  25863  lgsdir2lem4  25906  2sqb  26010  pntpbnd1  26164  ostthlem1  26205  hlbtwn  26399  cgracol  26616  inaghl  26633  brbtwn2  26693  axcontlem2  26753  isoun  30439  eliccelico  30502  elicoelioo  30503  fzsplit3  30519  prodpr  30544  xrge0iifhom  31182  esumsplit  31314  esumpad2  31317  sibfinima  31599  circlemethhgt  31916  bnj1137  32269  subfacp1lem4  32432  subfacp1lem5  32433  mclsax  32818  nosepdm  33190  nosupbnd2lem1  33217  poimirlem2  34896  poimirlem8  34902  poimirlem22  34916  poimirlem28  34922  ftc1cnnc  34968  ftc1anclem2  34970  eqfnun  34999  fdc  35022  incsequz2  35026  unichnidl  35311  lkrss2N  36307  cdlemg27b  37834  tendoex  38113  dihmeetlem2N  38437  dvh3dim3N  38587  rexzrexnn0  39408  pell14qrexpcl  39471  elpell1qr2  39476  acongeq  39587  jm2.23  39600  rpnnen3  39636  mnuprdlem3  40617  radcnvrat  40653  sumpair  41299  cncfiooicclem1  42183  fourierdlem80  42478  fourierdlem93  42491