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  944  stoic2a  1405  sbcied2  2946  csbied2  3047  elpw2g  4081  pofun  4234  tfi  4496  fnbr  5225  caovlem2d  5963  grprinvlem  5965  caofcom  6005  fnexALT  6011  tfr1onlemres  6246  tfrcllemres  6259  tfri3  6264  ixpexgg  6616  f1domg  6652  fundmfi  6826  f1ofi  6831  archnqq  7225  nqpru  7360  ltaddpr  7405  1idsr  7576  addgt0sr  7583  suplocsrlempr  7615  gt0ap0  8388  ap0gt0  8402  mulgt1  8621  gt0div  8628  ge0div  8629  ltdiv2  8645  creur  8717  avgle1  8960  recnz  9144  qreccl  9434  xrrege0  9608  peano2fzor  10009  flqltnz  10060  flqdiv  10094  zmodcl  10117  frecuzrdgtcl  10185  frecuzrdgfunlem  10192  seq3fveq  10244  ser3mono  10251  iseqf1olemkle  10257  seq3f1olemqsumkj  10271  seq3f1olemqsumk  10272  seq3id  10281  seq3z  10284  le2sq2  10368  bcpasc  10512  fihasheqf1oi  10534  seq3coll  10585  caucvgrelemcau  10752  caucvgre  10753  r19.2uz  10765  sqrtgt0  10806  xrmaxiflemval  11019  clim2ser  11106  clim2ser2  11107  climub  11113  serf0  11121  fsumf1o  11159  fisumss  11161  fsumcl2lem  11167  fsumsplit  11176  fsum2dlemstep  11203  fisumrev2  11215  fsumlessfi  11229  telfsumo  11235  fsumparts  11239  fsumiun  11246  binom1dif  11256  isumsplit  11260  isumrpcl  11263  isumlessdc  11265  explecnv  11274  cvgratnnlemmn  11294  cvgratz  11301  cvgratgt0  11302  mertenslemi1  11304  clim2prod  11308  clim2divap  11309  ef0lem  11366  eftlub  11396  tanval3ap  11421  dvdssubr  11539  divalgmod  11624  divgcdnn  11663  algfx  11733  eucalgcvga  11739  lcmcllem  11748  lcmneg  11755  isprm6  11825  cncongrprm  11835  phimullem  11901  tgcl  12233  tgclb  12234  tgss2  12248  ntrss3  12292  ntridm  12295  opnssneib  12325  ssnei2  12326  innei  12332  resttopon  12340  cnpnei  12388  cnntri  12393  lmss  12415  txcnp  12440  blpnfctr  12608  mopni2  12652  bdmopn  12673  climcncf  12740  ivthdec  12791  cnplimcim  12805  dvconst  12830  dvef  12856  cvgcmp2nlemabs  13227  trilpolemisumle  13231  trilpolemeq1  13233  trilpolemlt1  13234