MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  jaodan Structured version   Visualization version   GIF version

Theorem jaodan 957
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
StepHypRef Expression
1 jaodan.1 . . . 4 ((𝜑𝜓) → 𝜒)
21ex 414 . . 3 (𝜑 → (𝜓𝜒))
3 jaodan.2 . . . 4 ((𝜑𝜃) → 𝜒)
43ex 414 . . 3 (𝜑 → (𝜃𝜒))
52, 4jaod 858 . 2 (𝜑 → ((𝜓𝜃) → 𝜒))
65imp 408 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 397  wo 846
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 206  df-an 398  df-or 847
This theorem is referenced by:  mpjaodan  958  andi  1007  ccase  1037  mpjao3danOLD  1433  axpr  5388  relop  5811  poltletr  6091  ordnbtwn  6415  oeoa  8549  oeoe  8551  ssnnfi  9120  ssnnfiOLD  9121  domnsymfi  9154  phplem3OLD  9170  unwdomg  9527  numwdom  10002  infpssrlem5  10250  fin23lem24  10265  fin23lem28  10283  fin1a2lem10  10352  zornn0g  10448  gchdomtri  10572  fpwwe2lem11  10584  fpwwe2lem12  10585  msqgt0  11682  recextlem2  11793  lemul1a  12016  nnne0  12194  nnnn0addcl  12450  un0addcl  12453  un0mulcl  12454  elz2  12524  mul2lt0bi  13028  xaddnemnf  13162  xaddnepnf  13163  rexmul  13197  xlemul1a  13214  xrsupsslem  13233  xrinfmsslem  13234  ixxun  13287  fzsplit2  13473  fzsuc2  13506  elfzp12  13527  seqf1olem2  13955  expp1  13981  expneg  13982  expcllem  13985  mulexpz  14015  expaddz  14019  expmulz  14021  zzlesq  14117  faclbnd4lem3  14202  faclbnd4lem4  14203  faclbnd4  14204  bcpasc  14228  ccatass  14483  ccatrn  14484  ccatswrd  14563  ccatpfx  14596  cats1un  14616  revccat  14661  summo  15609  sumss2  15618  fsumsplit  15633  geomulcvg  15768  fprodsplit  15856  bpoly2  15947  bpoly3  15948  ef0lem  15968  odd2np1  16230  sadcaddlem  16344  gcdcllem3  16388  dvdslcm  16481  lcmeq0  16483  lcmcl  16484  lcmneg  16486  lcmgcd  16490  rpexp1i  16606  pcid  16752  4sqlem16  16839  funcres2c  17795  lubun  18411  mulgneg  18901  mulgnn0z  18910  frgpup3lem  19566  gsumzunsnd  19740  gsumunsnfd  19741  dprddisj2  19825  dmdprdsplit2  19832  dprdsplit  19834  gsumdixp  20040  lssvs0or  20587  evlslem4  21500  refun0  22882  txhaus  23014  xkoptsub  23021  ptunhmeo  23175  xpsxmetlem  23748  xpsmet  23751  mbfss  25026  itg1addlem2  25077  iblss2  25186  itgsplit  25216  limcres  25266  ftc1lem5  25420  coe1mul3  25480  dgrlt  25643  abelthlem3  25808  atanlogaddlem  26279  atanlogsub  26282  atans2  26297  efrlim  26335  bposlem2  26649  lgsdir2lem4  26692  2sqb  26796  pntpbnd1  26950  ostthlem1  26991  nosepdm  27048  nosupbnd2lem1  27079  negsid  27361  hlbtwn  27595  cgracol  27812  inaghl  27829  brbtwn2  27896  axcontlem2  27956  isoun  31657  eliccelico  31722  elicoelioo  31723  fzsplit3  31739  prodpr  31764  zarclsun  32491  xrge0iifhom  32558  esumsplit  32692  esumpad2  32695  sibfinima  32979  circlemethhgt  33296  bnj1137  33647  subfacp1lem4  33817  subfacp1lem5  33818  mclsax  34203  poimirlem2  36109  poimirlem8  36115  poimirlem22  36129  poimirlem28  36135  ftc1cnnc  36179  ftc1anclem2  36181  eqfnun  36210  fdc  36233  incsequz2  36237  unichnidl  36519  lkrss2N  37660  cdlemg27b  39188  tendoex  39467  dihmeetlem2N  39791  dvh3dim3N  39941  aks6d1c2p2  40578  sticksstones1  40583  sticksstones2  40584  metakunt9  40614  ofun  40689  sn-nnne0  40946  nn0addcom  40948  nn0mulcom  40952  zmulcomlem  40953  rexzrexnn0  41156  pell14qrexpcl  41219  elpell1qr2  41224  acongeq  41336  jm2.23  41349  rpnnen3  41385  mnringmulrcld  42582  mnuprdlem3  42628  radcnvrat  42668  sumpair  43314  cncfiooicclem1  44208  fourierdlem80  44501  fourierdlem93  44514  fullthinc  47140
  Copyright terms: Public domain W3C validator