Theorem syldan 282

Description: A syllogism deduction with conjoined antecents. (Contributed by NM, 24-Feb-2005.) (Proof shortened by Wolf Lammen, 6-Apr-2013.)

Hypotheses

Ref	Expression
syldan.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)
syldan.2	⊢ ((𝜑 ∧ 𝜒) → 𝜃)

Assertion

Ref	Expression
syldan	⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Proof of Theorem syldan

Step	Hyp	Ref	Expression
1		syldan.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2		syldan.2	. . . 4 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
3	2	expcom 116	. . 3 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	adantrd 279	. 2 ⊢ (𝜒 → ((𝜑 ∧ 𝜓) → 𝜃))
5	1, 4	mpcom 36	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia3 108

This theorem is referenced by:  sylan2  286  dn1dc  960  stoic2a  1429  sbcied2  3000  csbied2  3104  elpw2g  4156  pofun  4312  tfi  4581  fnbr  5318  caovlem2d  6066  caofcom  6105  fnexALT  6111  tfr1onlemres  6349  tfrcllemres  6362  tfri3  6367  ixpexgg  6721  f1domg  6757  fundmfi  6936  f1ofi  6941  archnqq  7415  nqpru  7550  ltaddpr  7595  1idsr  7766  addgt0sr  7773  suplocsrlempr  7805  gt0ap0  8582  ap0gt0  8596  mulgt1  8819  gt0div  8826  ge0div  8827  ltdiv2  8843  creur  8915  avgle1  9158  recnz  9345  qreccl  9641  xrrege0  9824  peano2fzor  10231  flqltnz  10286  flqdiv  10320  zmodcl  10343  frecuzrdgtcl  10411  frecuzrdgfunlem  10418  seq3fveq  10470  ser3mono  10477  iseqf1olemkle  10483  seq3f1olemqsumkj  10497  seq3f1olemqsumk  10498  seq3id  10507  seq3z  10510  le2sq2  10595  bcpasc  10745  fihasheqf1oi  10766  seq3coll  10821  caucvgrelemcau  10988  caucvgre  10989  r19.2uz  11001  sqrtgt0  11042  xrmaxiflemval  11257  clim2ser  11344  clim2ser2  11345  climub  11351  serf0  11359  fsumf1o  11397  fisumss  11399  fsumcl2lem  11405  fsumsplit  11414  fsum2dlemstep  11441  fisumrev2  11453  fsumlessfi  11467  telfsumo  11473  fsumparts  11477  fsumiun  11484  binom1dif  11494  isumsplit  11498  isumrpcl  11501  isumlessdc  11503  explecnv  11512  cvgratnnlemmn  11532  cvgratz  11539  cvgratgt0  11540  mertenslemi1  11542  clim2prod  11546  clim2divap  11547  fprodseq  11590  fprodf1o  11595  prodssdc  11596  fprodssdc  11597  fprodsplitdc  11603  fprodeq0  11624  fprod2dlemstep  11629  ef0lem  11667  eftlub  11697  tanval3ap  11721  dvdssubr  11845  divalgmod  11931  divgcdnn  11975  algfx  12051  eucalgcvga  12057  lcmcllem  12066  lcmneg  12073  isprm6  12146  cncongrprm  12156  phimullem  12224  pcid  12322  pcgcd  12327  pcz  12330  4sqlem9  12383  imasex  12725  grpidd  12801  ismndd  12837  grpinvid1  12923  grpinvid2  12924  grplcan  12931  grpinvinv  12936  grpinvval2  12952  mulgass  13018  mulgpropdg  13023  subginv  13039  subgmulg  13046  issubg2m  13047  issubg4m  13051  subsubg  13055  eqger  13081  ringidss  13210  isringd  13218  ringlz  13220  ringrz  13221  unitgrp  13283  0unit  13296  unitnegcl  13297  dvrass  13306  dvreq1  13309  dvrdir  13310  ringinvdv  13312  invrpropdg  13316  subrg1  13350  issubrg2  13360  subsubrg  13364  zringmulg  13458  tgcl  13534  tgclb  13535  tgss2  13549  ntrss3  13593  ntridm  13596  opnssneib  13626  ssnei2  13627  innei  13633  resttopon  13641  cnpnei  13689  cnntri  13694  lmss  13716  txcnp  13741  blpnfctr  13909  mopni2  13953  bdmopn  13974  climcncf  14041  ivthdec  14092  cnplimcim  14106  dvconst  14131  dvef  14158  rpcxpneg  14298  abscxp  14305  lgscllem  14378  lgsvalmod  14390  lgsdir2  14404  cvgcmp2nlemabs  14750  trilpolemisumle  14756  trilpolemeq1  14758  trilpolemlt1  14759  nconstwlpolemgt0  14781  neapmkvlem  14784