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  5374  relop  5805  poltletr  6095  ordnbtwn  6418  eqfnun  6989  oeoa  8533  oeoe  8535  ssnnfi  9104  domnsymfi  9134  unwdomg  9499  numwdom  9981  infpssrlem5  10229  fin23lem24  10244  fin23lem28  10262  fin1a2lem10  10331  zornn0g  10427  gchdomtri  10552  fpwwe2lem11  10564  fpwwe2lem12  10565  msqgt0  11670  recextlem2  11781  lemul1a  12009  nnne0  12211  nnnn0addcl  12467  un0addcl  12470  un0mulcl  12471  elz2  12542  mul2lt0bi  13050  xaddnemnf  13188  xaddnepnf  13189  rexmul  13223  xlemul1a  13240  xrsupsslem  13259  xrinfmsslem  13260  ixxun  13314  fzsplit2  13503  fzsuc2  13536  elfzp12  13557  seqf1olem2  14004  expp1  14030  expneg  14031  expcllem  14034  mulexpz  14064  expaddz  14068  expmulz  14070  zzlesq  14168  faclbnd4lem3  14257  faclbnd4lem4  14258  faclbnd4  14259  bcpasc  14283  ccatass  14551  ccatrn  14552  ccatswrd  14631  ccatpfx  14663  cats1un  14683  revccat  14728  summo  15679  sumss2  15688  fsumsplit  15703  geomulcvg  15841  fprodsplit  15931  bpoly2  16022  bpoly3  16023  ef0lem  16043  odd2np1  16310  sadcaddlem  16426  gcdcllem3  16470  dvdslcm  16567  lcmeq0  16569  lcmcl  16570  lcmneg  16572  lcmgcd  16576  rpexp1i  16693  pcid  16844  4sqlem16  16931  funcres2c  17870  lubun  18481  mulgneg  19068  mulgnn0z  19077  frgpup3lem  19752  gsumzunsnd  19931  gsumunsnfd  19932  dprddisj2  20016  dmdprdsplit2  20023  dprdsplit  20025  gsumdixp  20298  lssvs0or  21108  evlslem4  22054  refun0  23480  txhaus  23612  xkoptsub  23619  ptunhmeo  23773  xpsxmetlem  24344  xpsmet  24347  mbfss  25613  itg1addlem2  25664  iblss2  25773  itgsplit  25803  limcres  25853  ftc1lem5  26007  coe1mul3  26064  dgrlt  26231  abelthlem3  26398  atanlogaddlem  26877  atanlogsub  26880  atans2  26895  efrlim  26933  bposlem2  27248  lgsdir2lem4  27291  2sqb  27395  pntpbnd1  27549  ostthlem1  27590  nosepdm  27648  nosupbnd2lem1  27679  negsid  28033  elzn0s  28390  zsbday  28398  zcuts  28399  expsp1  28421  hlbtwn  28679  cgracol  28896  inaghl  28913  brbtwn2  28974  axcontlem2  29034  ifnebib  32619  isoun  32775  eliccelico  32850  elicoelioo  32851  fzsplit3  32866  prodpr  32899  zarclsun  34014  xrge0iifhom  34081  esumsplit  34197  esumpad2  34200  sibfinima  34483  circlemethhgt  34787  bnj1137  35137  subfacp1lem4  35365  subfacp1lem5  35366  mclsax  35751  poimirlem2  37943  poimirlem8  37949  poimirlem22  37963  poimirlem28  37969  ftc1cnnc  38013  ftc1anclem2  38015  fdc  38066  incsequz2  38070  unichnidl  38352  lkrss2N  39615  cdlemg27b  41142  tendoex  41421  dihmeetlem2N  41745  dvh3dim3N  41895  aks6d1c2p2  42558  hashscontpow  42561  aks6d1c5  42578  sticksstones1  42585  sticksstones2  42586  unitscyglem2  42635  ofun  42677  sn-nnne0  42905  nn0addcom  42907  nn0mulcom  42911  zmulcomlem  42912  rexzrexnn0  43232  pell14qrexpcl  43295  elpell1qr2  43300  acongeq  43411  jm2.23  43424  rpnnen3  43460  mnringmulrcld  44655  mnuprdlem3  44701  radcnvrat  44741  sumpair  45466  cncfiooicclem1  46321  fourierdlem80  46614  fourierdlem93  46627  fullthinc  49925