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  962  stoic2a  1440  sbcied2  3027  csbied2  3132  elpw2g  4190  pofun  4348  tfi  4619  fnbr  5363  caovlem2d  6120  caofcom  6170  fnexALT  6177  tfr1onlemres  6416  tfrcllemres  6429  tfri3  6434  ixpexgg  6790  f1domg  6826  fundmfi  7012  f1ofi  7018  finacn  7287  archnqq  7501  nqpru  7636  ltaddpr  7681  1idsr  7852  addgt0sr  7859  suplocsrlempr  7891  gt0ap0  8670  ap0gt0  8684  mulgt1  8907  gt0div  8914  ge0div  8915  ltdiv2  8931  creur  9003  avgle1  9249  recnz  9436  qreccl  9733  xrrege0  9917  peano2fzor  10325  flqltnz  10394  flqdiv  10430  zmodcl  10453  frecuzrdgtcl  10521  frecuzrdgfunlem  10528  seqfveqg  10587  seq3fveq  10588  ser3mono  10596  seqsplitg  10598  seqcaopr2g  10603  iseqf1olemkle  10606  seq3f1olemqsumkj  10620  seq3f1olemqsumk  10621  seqf1oglem2  10629  seqf1og  10630  seq3id  10634  seq3z  10637  seqhomog  10639  le2sq2  10724  bcpasc  10875  fihasheqf1oi  10896  seq3coll  10951  wrdnval  10982  wrdsymb1  10988  caucvgrelemcau  11162  caucvgre  11163  r19.2uz  11175  sqrtgt0  11216  xrmaxiflemval  11432  clim2ser  11519  clim2ser2  11520  climub  11526  serf0  11534  fsumf1o  11572  fisumss  11574  fsumcl2lem  11580  fsumsplit  11589  fsum2dlemstep  11616  fisumrev2  11628  fsumlessfi  11642  telfsumo  11648  fsumparts  11652  fsumiun  11659  binom1dif  11669  isumsplit  11673  isumrpcl  11676  isumlessdc  11678  explecnv  11687  cvgratnnlemmn  11707  cvgratz  11714  cvgratgt0  11715  mertenslemi1  11717  clim2prod  11721  clim2divap  11722  fprodseq  11765  fprodf1o  11770  prodssdc  11771  fprodssdc  11772  fprodsplitdc  11778  fprodeq0  11799  fprod2dlemstep  11804  ef0lem  11842  eftlub  11872  tanval3ap  11896  dvdssubr  12021  divalgmod  12109  bitsdc  12129  bitsp1  12133  divgcdnn  12167  algfx  12245  eucalgcvga  12251  lcmcllem  12260  lcmneg  12267  isprm6  12340  cncongrprm  12350  phimullem  12418  pcid  12518  pcgcd  12523  pcz  12526  4sqlem9  12580  4sqlem15  12599  4sqlem16  12600  imasex  13007  grpidd  13085  gsumress  13097  ismndd  13139  subsubm  13185  grpinvid1  13254  grpinvid2  13255  grplcan  13264  grpinvinv  13269  grpinvval2  13285  mulgass  13365  mulgpropdg  13370  subginv  13387  subgmulg  13394  issubg2m  13395  issubg4m  13399  subsubg  13403  eqger  13430  qusinv  13442  resghm  13466  conjsubgen  13484  rngrz  13578  isrngd  13585  ringidss  13661  isringd  13673  ringlz  13675  ringrz  13676  unitgrp  13748  0unit  13761  unitnegcl  13762  dvrass  13771  dvreq1  13774  dvrdir  13775  ringinvdv  13777  invrpropdg  13781  rhmunitinv  13810  issubrng2  13842  subsubrng  13846  subrg1  13863  issubrg2  13873  subsubrg  13877  lmod0vs  13953  lmodvs0  13954  lmodvneg1  13962  islss3  14011  lspsnsubg  14028  lspid  14029  lspssv  14030  lspidm  14033  lspsnneg  14052  sraval  14069  qus1  14158  zringmulg  14230  mulgrhm  14241  znidom  14289  tgcl  14384  tgclb  14385  tgss2  14399  ntrss3  14443  ntridm  14446  opnssneib  14476  ssnei2  14477  innei  14483  resttopon  14491  cnpnei  14539  cnntri  14544  lmss  14566  txcnp  14591  blpnfctr  14759  mopni2  14803  bdmopn  14824  climcncf  14904  ivthdec  14964  cnplimcim  14987  dvconst  15014  dvconstre  15016  dvef  15047  plymullem  15070  plycoeid3  15077  rpcxpneg  15227  abscxp  15235  sgmmul  15316  lgscllem  15332  lgsvalmod  15344  lgsdir2  15358  lgsquadlem2  15403  lgsquad2lem2  15407  cvgcmp2nlemabs  15763  trilpolemisumle  15769  trilpolemeq1  15771  trilpolemlt1  15772  nconstwlpolemgt0  15795  neapmkvlem  15798