Theorem ad2ant2r 494

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

Hypothesis

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

Assertion

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

Proof of Theorem ad2ant2r

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrr 464	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 462	1 ⊢ (((𝜑 ∧ 𝜃) ∧ (𝜓 ∧ 𝜏)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 103

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

This theorem is referenced by:  foco  5278  fvco4  5411  fliftfun  5613  f1imaen2g  6590  fodju0  6890  mulcomnqg  7039  mulassnqg  7040  ltdcnq  7053  lt2addnq  7060  lt2mulnq  7061  enq0ref  7089  enq0tr  7090  addcmpblnq0  7099  nqpnq0nq  7109  nqnq0m  7111  mulcomnq0  7116  addlocpr  7192  nqprl  7207  nqpru  7208  prmuloc  7222  distrlem1prl  7238  distrlem1pru  7239  ltaddpr  7253  ltexprlemopu  7259  ltexprlemdisj  7262  ltexprlemloc  7263  ltexprlemrl  7266  ltexprlemru  7268  recexprlemloc  7287  recexprlem1ssl  7289  recexprlem1ssu  7290  caucvgprprlemopu  7355  addcomsrg  7398  mulcomsrg  7400  mulasssrg  7401  distrsrg  7402  addcnsr  7468  mulcnsr  7469  addcnsrec  7476  axaddcl  7498  axaddcom  7502  addsub4  7822  muladd  7959  mullt0  8055  apreim  8177  mulge0  8193  divmuldivap  8276  divmul24ap  8280  divmuleqap  8281  recdivap  8282  divadddivap  8291  conjmulap  8293  prodgt0gt0  8409  ltmul12a  8418  lemul12b  8419  lediv2a  8453  qmulcl  9221  irrmul  9231  xrrege0  9391  ge0addcl  9547  ge0mulcl  9548  ge0xaddcl  9549  fzass4  9625  fzrev  9647  fzocatel  9759  expclzaplem  10094  expge0  10106  expge1  10107  lt2sq  10143  le2sq  10144  bernneq  10189  sq11ap  10235  sqrt11ap  10586  2clim  10844  climge0  10868  tanaddaplem  11178  opeo  11324  omeo  11325  cncongr1  11512  setscom  11683  opnneissb  12007  cncnpi  12079