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  5737  mpofun  6123  xpdom2  7015  addcmpblnq  7587  addpipqqslem  7589  addpipqqs  7590  addclnq  7595  addcomnqg  7601  addassnqg  7602  mulcomnqg  7603  mulassnqg  7604  distrnqg  7607  ltdcnq  7617  enq0ref  7653  addcmpblnq0  7663  addclnq0  7671  nqpnq0nq  7673  nqnq0a  7674  nqnq0m  7675  distrnq0  7679  mulcomnq0  7680  addassnq0lemcl  7681  genpdisj  7743  appdiv0nq  7784  addcomsrg  7975  mulcomsrg  7977  mulasssrg  7978  distrsrg  7979  addcnsr  8054  mulcnsr  8055  addcnsrec  8062  axaddcl  8084  axmulcl  8086  axaddcom  8090  add42  8341  muladd  8563  mulsub  8580  apreim  8783  divmuleqap  8897  ltmul12a  9040  lemul12b  9041  lemul12a  9042  qaddcl  9869  qmulcl  9871  iooshf  10187  fzass4  10297  elfzomelpfzo  10477  swrdccatin2  11314  pfxccatin12  11318  tanaddaplem  12304  issubg4m  13785  ghmpreima  13858  islmodd  14313  opnneissb  14885  neitx  14998  txcnmpt  15003  txrest  15006  metcnp3  15241  cncfmet  15322  dveflem  15456  lgsdir2  15768