Theorem ad2ant2l 508

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 478	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 476	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

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

This theorem is referenced by:  mpteqb  5688  mpofun  6065  xpdom2  6946  addcmpblnq  7510  addpipqqslem  7512  addpipqqs  7513  addclnq  7518  addcomnqg  7524  addassnqg  7525  mulcomnqg  7526  mulassnqg  7527  distrnqg  7530  ltdcnq  7540  enq0ref  7576  addcmpblnq0  7586  addclnq0  7594  nqpnq0nq  7596  nqnq0a  7597  nqnq0m  7598  distrnq0  7602  mulcomnq0  7603  addassnq0lemcl  7604  genpdisj  7666  appdiv0nq  7707  addcomsrg  7898  mulcomsrg  7900  mulasssrg  7901  distrsrg  7902  addcnsr  7977  mulcnsr  7978  addcnsrec  7985  axaddcl  8007  axmulcl  8009  axaddcom  8013  add42  8264  muladd  8486  mulsub  8503  apreim  8706  divmuleqap  8820  ltmul12a  8963  lemul12b  8964  lemul12a  8965  qaddcl  9786  qmulcl  9788  iooshf  10104  fzass4  10214  elfzomelpfzo  10392  tanaddaplem  12134  issubg4m  13614  ghmpreima  13687  islmodd  14140  opnneissb  14712  neitx  14825  txcnmpt  14830  txrest  14833  metcnp3  15068  cncfmet  15149  dveflem  15283  lgsdir2  15595