Theorem ad2ant2lr 744

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 23-Nov-2007.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2lr	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Proof of Theorem ad2ant2lr

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 713	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantll 710	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 206  df-an 396

This theorem is referenced by:  mpteqb  6876  omxpenlem  8813  fineqvlem  8966  marypha1lem  9122  fin23lem26  10012  axdc3lem4  10140  mulcmpblnr  10758  ltsrpr  10764  sub4  11196  muladd  11337  ltleadd  11388  divdivdiv  11606  divadddiv  11620  ltmul12a  11761  lt2mul2div  11783  xlemul1a  12951  fzrev  13248  facndiv  13930  fsumconst  15430  fprodconst  15616  isprm5  16340  acsfn2  17289  ghmeql  18772  subgdmdprd  19552  lssvsubcl  20120  lssvacl  20131  ocvin  20791  lindfmm  20944  scmatghm  21590  scmatmhm  21591  slesolinv  21737  slesolinvbi  21738  slesolex  21739  pm2mpf1lem  21851  pm2mpcoe1  21857  reftr  22573  alexsubALTlem2  23107  alexsubALTlem3  23108  blbas  23491  nmoco  23807  cncfmet  23978  cmetcaulem  24357  mbflimsup  24735  ulmdvlem3  25466  ptolemy  25558  3wlkdlem6  28430  vdn0conngrumgrv2  28461  frgrncvvdeqlem8  28571  frgrwopreglem5ALT  28587  grpoideu  28772  ipblnfi  29118  htthlem  29180  hvaddsub4  29341  bralnfn  30211  hmops  30283  hmopm  30284  adjadd  30356  opsqrlem1  30403  atomli  30645  chirredlem2  30654  atcvat3i  30659  mdsymlem5  30670  cdj1i  30696  derangenlem  33033  elmrsubrn  33382  dfon2lem6  33670  poseq  33729  sltsolem1  33805  madebdaylemlrcut  34006  pibt2  35515  matunitlindflem1  35700  mblfinlem1  35741  prdsbnd  35878  heibor1lem  35894  hl2at  37346  congneg  40707  jm2.26  40740  stoweidlem34  43465  fmtnofac2lem  44908  lindslinindsimp2  45692  ltsubaddb  45743  ltsubadd2b  45745  aacllem  46391