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  3015  csbied2  3119  elpw2g  4171  pofun  4327  tfi  4596  fnbr  5334  caovlem2d  6085  caofcom  6125  fnexALT  6131  tfr1onlemres  6369  tfrcllemres  6382  tfri3  6387  ixpexgg  6743  f1domg  6779  fundmfi  6962  f1ofi  6967  archnqq  7441  nqpru  7576  ltaddpr  7621  1idsr  7792  addgt0sr  7799  suplocsrlempr  7831  gt0ap0  8608  ap0gt0  8622  mulgt1  8845  gt0div  8852  ge0div  8853  ltdiv2  8869  creur  8941  avgle1  9184  recnz  9371  qreccl  9667  xrrege0  9850  peano2fzor  10257  flqltnz  10313  flqdiv  10347  zmodcl  10370  frecuzrdgtcl  10438  frecuzrdgfunlem  10445  seq3fveq  10497  ser3mono  10504  iseqf1olemkle  10510  seq3f1olemqsumkj  10524  seq3f1olemqsumk  10525  seq3id  10534  seq3z  10537  le2sq2  10622  bcpasc  10773  fihasheqf1oi  10794  seq3coll  10849  caucvgrelemcau  11016  caucvgre  11017  r19.2uz  11029  sqrtgt0  11070  xrmaxiflemval  11285  clim2ser  11372  clim2ser2  11373  climub  11379  serf0  11387  fsumf1o  11425  fisumss  11427  fsumcl2lem  11433  fsumsplit  11442  fsum2dlemstep  11469  fisumrev2  11481  fsumlessfi  11495  telfsumo  11501  fsumparts  11505  fsumiun  11512  binom1dif  11522  isumsplit  11526  isumrpcl  11529  isumlessdc  11531  explecnv  11540  cvgratnnlemmn  11560  cvgratz  11567  cvgratgt0  11568  mertenslemi1  11570  clim2prod  11574  clim2divap  11575  fprodseq  11618  fprodf1o  11623  prodssdc  11624  fprodssdc  11625  fprodsplitdc  11631  fprodeq0  11652  fprod2dlemstep  11657  ef0lem  11695  eftlub  11725  tanval3ap  11749  dvdssubr  11873  divalgmod  11959  divgcdnn  12003  algfx  12079  eucalgcvga  12085  lcmcllem  12094  lcmneg  12101  isprm6  12174  cncongrprm  12184  phimullem  12252  pcid  12351  pcgcd  12356  pcz  12359  4sqlem9  12413  4sqlem15  12432  4sqlem16  12433  imasex  12775  grpidd  12852  ismndd  12891  subsubm  12928  grpinvid1  12989  grpinvid2  12990  grplcan  12999  grpinvinv  13004  grpinvval2  13020  mulgass  13092  mulgpropdg  13097  subginv  13113  subgmulg  13120  issubg2m  13121  issubg4m  13125  subsubg  13129  eqger  13156  qusinv  13168  resghm  13192  conjsubgen  13210  rngrz  13293  isrngd  13300  ringidss  13376  isringd  13388  ringlz  13390  ringrz  13391  unitgrp  13459  0unit  13472  unitnegcl  13473  dvrass  13482  dvreq1  13485  dvrdir  13486  ringinvdv  13488  invrpropdg  13492  rhmunitinv  13521  issubrng2  13550  subsubrng  13554  subrg1  13571  issubrg2  13581  subsubrg  13585  lmod0vs  13630  lmodvs0  13631  lmodvneg1  13639  islss3  13688  lspsnsubg  13705  lspid  13706  lspssv  13707  lspidm  13710  lspsnneg  13729  sraval  13746  qus1  13834  zringmulg  13890  mulgrhm  13900  tgcl  14001  tgclb  14002  tgss2  14016  ntrss3  14060  ntridm  14063  opnssneib  14093  ssnei2  14094  innei  14100  resttopon  14108  cnpnei  14156  cnntri  14161  lmss  14183  txcnp  14208  blpnfctr  14376  mopni2  14420  bdmopn  14441  climcncf  14508  ivthdec  14559  cnplimcim  14573  dvconst  14598  dvef  14625  rpcxpneg  14765  abscxp  14772  lgscllem  14845  lgsvalmod  14857  lgsdir2  14871  cvgcmp2nlemabs  15218  trilpolemisumle  15224  trilpolemeq1  15226  trilpolemlt1  15227  nconstwlpolemgt0  15250  neapmkvlem  15253