Theorem syldan 280

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 115	. . 3 ⊢ (𝜒 → (𝜑 → 𝜃))
4	3	adantrd 277	. 2 ⊢ (𝜒 → ((𝜑 ∧ 𝜓) → 𝜃))
5	1, 4	mpcom 36	1 ⊢ ((𝜑 ∧ 𝜓) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylan2  284  dn1dc  949  stoic2a  1416  sbcied2  2983  csbied2  3087  elpw2g  4129  pofun  4284  tfi  4553  fnbr  5284  caovlem2d  6025  grprinvlem  6027  caofcom  6067  fnexALT  6073  tfr1onlemres  6308  tfrcllemres  6321  tfri3  6326  ixpexgg  6679  f1domg  6715  fundmfi  6894  f1ofi  6899  archnqq  7349  nqpru  7484  ltaddpr  7529  1idsr  7700  addgt0sr  7707  suplocsrlempr  7739  gt0ap0  8515  ap0gt0  8529  mulgt1  8749  gt0div  8756  ge0div  8757  ltdiv2  8773  creur  8845  avgle1  9088  recnz  9275  qreccl  9571  xrrege0  9752  peano2fzor  10157  flqltnz  10212  flqdiv  10246  zmodcl  10269  frecuzrdgtcl  10337  frecuzrdgfunlem  10344  seq3fveq  10396  ser3mono  10403  iseqf1olemkle  10409  seq3f1olemqsumkj  10423  seq3f1olemqsumk  10424  seq3id  10433  seq3z  10436  le2sq2  10520  bcpasc  10668  fihasheqf1oi  10690  seq3coll  10741  caucvgrelemcau  10908  caucvgre  10909  r19.2uz  10921  sqrtgt0  10962  xrmaxiflemval  11177  clim2ser  11264  clim2ser2  11265  climub  11271  serf0  11279  fsumf1o  11317  fisumss  11319  fsumcl2lem  11325  fsumsplit  11334  fsum2dlemstep  11361  fisumrev2  11373  fsumlessfi  11387  telfsumo  11393  fsumparts  11397  fsumiun  11404  binom1dif  11414  isumsplit  11418  isumrpcl  11421  isumlessdc  11423  explecnv  11432  cvgratnnlemmn  11452  cvgratz  11459  cvgratgt0  11460  mertenslemi1  11462  clim2prod  11466  clim2divap  11467  fprodseq  11510  fprodf1o  11515  prodssdc  11516  fprodssdc  11517  fprodsplitdc  11523  fprodeq0  11544  fprod2dlemstep  11549  ef0lem  11587  eftlub  11617  tanval3ap  11641  dvdssubr  11764  divalgmod  11849  divgcdnn  11893  algfx  11963  eucalgcvga  11969  lcmcllem  11978  lcmneg  11985  isprm6  12056  cncongrprm  12066  phimullem  12134  pcid  12232  pcgcd  12237  pcz  12240  tgcl  12605  tgclb  12606  tgss2  12620  ntrss3  12664  ntridm  12667  opnssneib  12697  ssnei2  12698  innei  12704  resttopon  12712  cnpnei  12760  cnntri  12765  lmss  12787  txcnp  12812  blpnfctr  12980  mopni2  13024  bdmopn  13045  climcncf  13112  ivthdec  13163  cnplimcim  13177  dvconst  13202  dvef  13229  rpcxpneg  13369  abscxp  13376  cvgcmp2nlemabs  13745  trilpolemisumle  13751  trilpolemeq1  13753  trilpolemlt1  13754  nconstwlpolemgt0  13776  neapmkvlem  13779