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  5648  mpofun  6020  xpdom2  6885  addcmpblnq  7427  addpipqqslem  7429  addpipqqs  7430  addclnq  7435  addcomnqg  7441  addassnqg  7442  mulcomnqg  7443  mulassnqg  7444  distrnqg  7447  ltdcnq  7457  enq0ref  7493  addcmpblnq0  7503  addclnq0  7511  nqpnq0nq  7513  nqnq0a  7514  nqnq0m  7515  distrnq0  7519  mulcomnq0  7520  addassnq0lemcl  7521  genpdisj  7583  appdiv0nq  7624  addcomsrg  7815  mulcomsrg  7817  mulasssrg  7818  distrsrg  7819  addcnsr  7894  mulcnsr  7895  addcnsrec  7902  axaddcl  7924  axmulcl  7926  axaddcom  7930  add42  8181  muladd  8403  mulsub  8420  apreim  8622  divmuleqap  8736  ltmul12a  8879  lemul12b  8880  lemul12a  8881  qaddcl  9700  qmulcl  9702  iooshf  10018  fzass4  10128  elfzomelpfzo  10298  tanaddaplem  11881  issubg4m  13263  ghmpreima  13336  islmodd  13789  opnneissb  14323  neitx  14436  txcnmpt  14441  txrest  14444  metcnp3  14679  cncfmet  14747  dveflem  14872  lgsdir2  15149