Theorem jaodan 972

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∨ wo 861

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-or 862

This theorem is used by:  mpjaodan  973  andi  1025  ccase  1053  axprOLD  5397  relop  5830  poltletr  6126  ordnbtwn  6453  eqfnun  7030  oeoa  8586  oeoe  8588  ssnnfi  9165  domnsymfi  9195  unwdomg  9557  numwdom  10063  infpssrlem5  10310  fin23lem24  10325  fin23lem28  10343  fin1a2lem10  10412  zornn0g  10508  gchdomtri  10639  fpwwe2lem11  10651  fpwwe2lem12  10652  msqgt0  11759  recextlem2  11870  lemul1a  12094  nnne0  12295  nnnn0addcl  12559  un0addcl  12562  un0mulcl  12563  elz2  12634  mul2lt0bi  13151  xaddnemnf  13289  xaddnepnf  13290  rexmul  13324  xlemul1a  13341  xrsupsslem  13360  xrinfmsslem  13361  ixxun  13415  fzsplit2  13605  fzsuc2  13638  elfzp12  13659  seqf1olem2  14107  expp1  14133  expneg  14134  expcllem  14137  mulexpz  14167  expaddz  14171  expmulz  14173  zzlesq  14271  faclbnd4lem3  14360  faclbnd4lem4  14361  faclbnd4  14362  bcpasc  14386  ccatass  14655  ccatrn  14656  ccatswrd  14739  ccatpfx  14771  cats1un  14791  revccat  14836  summo  15804  sumss2  15813  fsumsplit  15828  geomulcvg  15966  fprodsplit  16054  bpoly2  16144  bpoly3  16145  ef0lem  16165  odd2np1  16432  sadcaddlem  16548  gcdcllem3  16592  dvdslcm  16689  lcmeq0  16691  lcmcl  16692  lcmneg  16694  lcmgcd  16698  rpexp1i  16815  pcid  16966  4sqlem16  17053  funcres2c  17993  lubun  18604  mulgneg  19216  mulgnn0z  19225  frgpup3lem  19905  gsumzunsnd  20084  gsumunsnfd  20085  dprddisj2  20169  dmdprdsplit2  20176  dprdsplit  20178  gsumdixp  20460  lssvs0or  21298  evlslem4  22293  refun0  23742  txhaus  23874  xkoptsub  23881  ptunhmeo  24035  xpsxmetlem  24606  xpsmet  24609  mbfss  25875  itg1addlem2  25926  iblss2  26034  itgsplit  26064  limcres  26114  ftc1lem5  26268  coe1mul3  26325  dgrlt  26493  abelthlem3  26670  atanlogaddlem  27151  atanlogsub  27154  atans2  27169  efrlim  27207  bposlem2  27522  lgsdir2lem4  27565  2sqb  27669  pntpbnd1  27823  ostthlem1  27864  nosepdm  27921  nosupbnd2lem1  27952  negsid  28307  elzn0s  28664  zsbday  28672  zcuts  28673  expsp1  28695  hlbtwn  28957  cgracol  29216  inaghl  29244  brbtwn2  29363  axcontlem2  29423  ifnebib  33025  isoun  33175  eliccelico  33249  elicoelioo  33250  fzsplit3  33265  prodpr  33297  zarclsun  34381  xrge0iifhom  34448  esumsplit  34564  esumpad2  34567  sibfinima  34851  circlemethhgt  35152  bnj1137  35505  subfacp1lem4  35763  subfacp1lem5  35764  mclsax  36149  poimirlem2  38372  poimirlem8  38378  poimirlem22  38392  poimirlem28  38398  ftc1cnnc  38442  ftc1anclem2  38444  fdc  38496  incsequz2  38500  unichnidl  38782  lkrss2N  40043  cdlemg27b  41570  tendoex  41849  dihmeetlem2N  42173  dvh3dim3N  42323  aks6d1c2p2  42986  hashscontpow  42989  aks6d1c5  43006  sticksstones1  43013  sticksstones2  43014  unitscyglem2  43063  ofun  43106  sn-nnne0  43349  nn0addcom  43351  nn0mulcom  43355  zmulcomlem  43356  rexzrexnn0  43646  pell14qrexpcl  43709  elpell1qr2  43714  acongeq  43825  jm2.23  43838  rpnnen3  43874  mnringmulrcld  45067  mnuprdlem3  45099  radcnvrat  45139  sumpair  45870  cncfiooicclem1  46722  fourierdlem80  47015  fourierdlem93  47028  fullthinc  50377  veronesevrowd  50813