Theorem ad2ant2l 491

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

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

Assertion

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

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 461	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 459	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 102

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

This theorem is referenced by:  mpteqb  5282  mpt2fun  5623  xpdom2  6328  addcmpblnq  6557  addpipqqslem  6559  addpipqqs  6560  addclnq  6565  addcomnqg  6571  addassnqg  6572  mulcomnqg  6573  mulassnqg  6574  distrnqg  6577  ltdcnq  6587  enq0ref  6623  addcmpblnq0  6633  addclnq0  6641  nqpnq0nq  6643  nqnq0a  6644  nqnq0m  6645  distrnq0  6649  mulcomnq0  6650  addassnq0lemcl  6651  genpdisj  6713  appdiv0nq  6754  addcomsrg  6932  mulcomsrg  6934  mulasssrg  6935  distrsrg  6936  addcnsr  7002  mulcnsr  7003  addcnsrec  7010  axaddcl  7032  axmulcl  7034  axaddcom  7036  add42  7270  muladd  7488  mulsub  7505  apreim  7703  divmuleqap  7805  ltmul12a  7938  lemul12b  7939  lemul12a  7940  qaddcl  8720  qmulcl  8722  iooshf  8975  fzass4  9080  elfzomelpfzo  9240