Theorem jaodan 960

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

Syntax hints:   → wi 4   ∧ wa 395   ∨ wo 848

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 207  df-an 396  df-or 849

This theorem is referenced by:  mpjaodan  961  andi  1010  ccase  1038  axprOLD  5370  relop  5800  poltletr  6090  ordnbtwn  6413  eqfnun  6984  oeoa  8527  oeoe  8529  ssnnfi  9098  domnsymfi  9128  unwdomg  9493  numwdom  9975  infpssrlem5  10223  fin23lem24  10238  fin23lem28  10256  fin1a2lem10  10325  zornn0g  10421  gchdomtri  10546  fpwwe2lem11  10558  fpwwe2lem12  10559  msqgt0  11664  recextlem2  11775  lemul1a  12003  nnne0  12205  nnnn0addcl  12461  un0addcl  12464  un0mulcl  12465  elz2  12536  mul2lt0bi  13044  xaddnemnf  13182  xaddnepnf  13183  rexmul  13217  xlemul1a  13234  xrsupsslem  13253  xrinfmsslem  13254  ixxun  13308  fzsplit2  13497  fzsuc2  13530  elfzp12  13551  seqf1olem2  13998  expp1  14024  expneg  14025  expcllem  14028  mulexpz  14058  expaddz  14062  expmulz  14064  zzlesq  14162  faclbnd4lem3  14251  faclbnd4lem4  14252  faclbnd4  14253  bcpasc  14277  ccatass  14545  ccatrn  14546  ccatswrd  14625  ccatpfx  14657  cats1un  14677  revccat  14722  summo  15673  sumss2  15682  fsumsplit  15697  geomulcvg  15835  fprodsplit  15925  bpoly2  16016  bpoly3  16017  ef0lem  16037  odd2np1  16304  sadcaddlem  16420  gcdcllem3  16464  dvdslcm  16561  lcmeq0  16563  lcmcl  16564  lcmneg  16566  lcmgcd  16570  rpexp1i  16687  pcid  16838  4sqlem16  16925  funcres2c  17864  lubun  18475  mulgneg  19062  mulgnn0z  19071  frgpup3lem  19746  gsumzunsnd  19925  gsumunsnfd  19926  dprddisj2  20010  dmdprdsplit2  20017  dprdsplit  20019  gsumdixp  20292  lssvs0or  21103  evlslem4  22067  refun0  23493  txhaus  23625  xkoptsub  23632  ptunhmeo  23786  xpsxmetlem  24357  xpsmet  24360  mbfss  25626  itg1addlem2  25677  iblss2  25786  itgsplit  25816  limcres  25866  ftc1lem5  26020  coe1mul3  26077  dgrlt  26244  abelthlem3  26414  atanlogaddlem  26893  atanlogsub  26896  atans2  26911  efrlim  26949  efrlimOLD  26950  bposlem2  27265  lgsdir2lem4  27308  2sqb  27412  pntpbnd1  27566  ostthlem1  27607  nosepdm  27665  nosupbnd2lem1  27696  negsid  28050  elzn0s  28407  zsbday  28415  zcuts  28416  expsp1  28438  hlbtwn  28696  cgracol  28913  inaghl  28930  brbtwn2  28991  axcontlem2  29051  ifnebib  32637  isoun  32793  eliccelico  32868  elicoelioo  32869  fzsplit3  32884  prodpr  32917  zarclsun  34033  xrge0iifhom  34100  esumsplit  34216  esumpad2  34219  sibfinima  34502  circlemethhgt  34806  bnj1137  35156  subfacp1lem4  35384  subfacp1lem5  35385  mclsax  35770  poimirlem2  37960  poimirlem8  37966  poimirlem22  37980  poimirlem28  37986  ftc1cnnc  38030  ftc1anclem2  38032  fdc  38083  incsequz2  38087  unichnidl  38369  lkrss2N  39632  cdlemg27b  41159  tendoex  41438  dihmeetlem2N  41762  dvh3dim3N  41912  aks6d1c2p2  42575  hashscontpow  42578  aks6d1c5  42595  sticksstones1  42602  sticksstones2  42603  unitscyglem2  42652  ofun  42694  sn-nnne0  42922  nn0addcom  42924  nn0mulcom  42928  zmulcomlem  42929  rexzrexnn0  43253  pell14qrexpcl  43316  elpell1qr2  43321  acongeq  43432  jm2.23  43445  rpnnen3  43481  mnringmulrcld  44676  mnuprdlem3  44722  radcnvrat  44762  sumpair  45487  cncfiooicclem1  46342  fourierdlem80  46635  fourierdlem93  46648  fullthinc  49940