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  relop  5828  poltletr  6126  ordnbtwn  6458  eqfnun  7036  oeoa  8606  oeoe  8608  ssnnfi  9185  domnsymfi  9215  unwdomg  9578  numwdom  10138  infpssrlem5  10385  fin23lem24  10400  fin23lem28  10418  fin1a2lem10  10487  zornn0g  10583  gchdomtri  10714  fpwwe2lem11  10726  fpwwe2lem12  10727  msqgt0  11836  recextlem2  11947  lemul1a  12171  nnne0  12372  nnnn0addcl  12636  un0addcl  12639  un0mulcl  12640  elz2  12711  mul2lt0bi  13228  xaddnemnf  13366  xaddnepnf  13367  rexmul  13401  xlemul1a  13418  xrsupsslem  13437  xrinfmsslem  13438  ixxun  13492  fzsplit2  13683  fzsuc2  13716  elfzp12  13737  seqf1olem2  14185  expp1  14211  expneg  14212  expcllem  14215  mulexpz  14245  expaddz  14249  expmulz  14251  zzlesq  14350  faclbnd4lem3  14439  faclbnd4lem4  14440  faclbnd4  14441  bcpasc  14465  ccatass  14734  ccatrn  14735  ccatswrd  14818  ccatpfx  14850  cats1un  14870  revccat  14915  summo  15883  sumss2  15892  fsumsplit  15907  geomulcvg  16045  fprodsplit  16133  bpoly2  16223  bpoly3  16224  ef0lem  16244  odd2np1  16511  sadcaddlem  16627  gcdcllem3  16671  dvdslcm  16773  lcmeq0  16775  lcmcl  16776  lcmneg  16778  lcmgcd  16782  rpexp1i  16899  pcid  17051  4sqlem16  17138  funcres2c  18078  lubun  18689  mulgneg  19302  mulgnn0z  19311  frgpup3lem  19991  gsumzunsnd  20170  gsumunsnfd  20171  dprddisj2  20255  dmdprdsplit2  20262  dprdsplit  20264  gsumdixp  20548  lssvs0or  21388  evlslem4  22385  refun0  23834  txhaus  23966  xkoptsub  23973  ptunhmeo  24127  xpsxmetlem  24698  xpsmet  24701  mbfss  25967  itg1addlem2  26018  iblss2  26126  itgsplit  26156  limcres  26206  ftc1lem5  26360  coe1mul3  26417  dgrlt  26585  abelthlem3  26760  atanlogaddlem  27241  atanlogsub  27244  atans2  27259  efrlim  27297  bposlem2  27612  lgsdir2lem4  27655  2sqb  27759  pntpbnd1  27913  ostthlem1  27954  nosepdm  28041  nosupbnd2lem1  28072  negsid  28427  elzn0s  28784  zsbday  28792  zcuts  28793  expsp1  28815  hlbtwn  29077  cgracol  29336  inaghl  29364  brbtwn2  29483  axcontlem2  29543  ifnebib  33145  isoun  33295  eliccelico  33369  elicoelioo  33370  fzsplit3  33385  prodpr  33417  zarclsun  34502  xrge0iifhom  34569  esumsplit  34685  esumpad2  34688  sibfinima  34971  circlemethhgt  35272  bnj1137  35625  subfacp1lem4  35948  subfacp1lem5  35949  mclsax  36334  poimirlem2  38540  poimirlem8  38546  poimirlem22  38560  poimirlem28  38566  ftc1cnnc  38610  ftc1anclem2  38612  dfprop1  38645  fdc  38679  incsequz2  38683  unichnidl  38965  lkrss2N  40226  cdlemg27b  41753  tendoex  42032  dihmeetlem2N  42356  dvh3dim3N  42506  aks6d1c2p2  43169  hashscontpow  43172  aks6d1c5  43189  sticksstones1  43196  sticksstones2  43197  unitscyglem2  43246  ofun  43289  sn-nnne0  43524  nn0addcom  43526  nn0mulcom  43530  zmulcomlem  43531  rexzrexnn0  43810  pell14qrexpcl  43873  elpell1qr2  43878  acongeq  43989  jm2.23  44002  rpnnen3  44038  mnringmulrcld  45225  mnuprdlem3  45257  radcnvrat  45297  sumpair  46051  cncfiooicclem1  46902  fourierdlem80  47195  fourierdlem93  47208  fullthinc  50557  veronesevrowd  50978