Theorem syldan 278

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

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  sylan2  282  dn1dc  912  stoic2a  1373  sbcied2  2898  csbied2  2997  elpw2g  4021  pofun  4172  tfi  4434  fnbr  5161  caovlem2d  5895  grprinvlem  5897  caofcom  5936  fnexALT  5942  tfr1onlemres  6176  tfrcllemres  6189  tfri3  6194  ixpexgg  6546  f1domg  6582  fundmfi  6754  f1ofi  6759  archnqq  7126  nqpru  7261  ltaddpr  7306  1idsr  7464  addgt0sr  7471  gt0ap0  8254  ap0gt0  8267  mulgt1  8479  gt0div  8486  ge0div  8487  ltdiv2  8503  creur  8575  avgle1  8812  recnz  8996  qreccl  9284  xrrege0  9449  peano2fzor  9850  flqltnz  9901  flqdiv  9935  zmodcl  9958  frecuzrdgtcl  10026  frecuzrdgfunlem  10033  seq3fveq  10085  ser3mono  10092  iseqf1olemkle  10098  seq3f1olemqsumkj  10112  seq3f1olemqsumk  10113  seq3id  10122  seq3z  10125  le2sq2  10209  bcpasc  10353  fihasheqf1oi  10375  seq3coll  10426  caucvgrelemcau  10592  caucvgre  10593  r19.2uz  10605  sqrtgt0  10646  xrmaxiflemval  10858  clim2ser  10945  clim2ser2  10946  climub  10952  serf0  10960  fsumf1o  10998  fisumss  11000  fsumcl2lem  11006  fsumsplit  11015  fsum2dlemstep  11042  fisumrev2  11054  fsumlessfi  11068  telfsumo  11074  fsumparts  11078  fsumiun  11085  binom1dif  11095  isumsplit  11099  isumrpcl  11102  isumlessdc  11104  explecnv  11113  cvgratnnlemmn  11133  cvgratz  11140  cvgratgt0  11141  mertenslemi1  11143  ef0lem  11164  eftlub  11194  tanval3ap  11219  dvdssubr  11334  divalgmod  11419  divgcdnn  11458  algfx  11526  eucalgcvga  11532  lcmcllem  11541  lcmneg  11548  isprm6  11618  cncongrprm  11628  phimullem  11693  tgcl  12015  tgclb  12016  tgss2  12030  ntrss3  12074  ntridm  12077  opnssneib  12107  ssnei2  12108  innei  12114  resttopon  12122  cnpnei  12169  cnntri  12174  lmss  12196  txcnp  12221  blpnfctr  12367  mopni2  12411  bdmopn  12432  climcncf  12484  cnplimcim  12516  dvconst  12534  cvgcmp2nlemabs  12811  trilpolemisumle  12815  trilpolemeq1  12817  trilpolemlt1  12818