Theorem ad2ant2r 492

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 462	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜏)) → 𝜒)
3	2	adantlr 460	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:  foco  5136  fliftfun  5456  f1imaen2g  6296  mulcomnqg  6573  mulassnqg  6574  ltdcnq  6587  lt2addnq  6594  lt2mulnq  6595  enq0ref  6623  enq0tr  6624  addcmpblnq0  6633  nqpnq0nq  6643  nqnq0m  6645  mulcomnq0  6650  addlocpr  6726  nqprl  6741  nqpru  6742  prmuloc  6756  distrlem1prl  6772  distrlem1pru  6773  ltaddpr  6787  ltexprlemopu  6793  ltexprlemdisj  6796  ltexprlemloc  6797  ltexprlemrl  6800  ltexprlemru  6802  recexprlemloc  6821  recexprlem1ssl  6823  recexprlem1ssu  6824  caucvgprprlemopu  6889  addcomsrg  6932  mulcomsrg  6934  mulasssrg  6935  distrsrg  6936  addcnsr  7002  mulcnsr  7003  addcnsrec  7010  axaddcl  7032  axaddcom  7036  addsub4  7351  muladd  7488  mullt0  7584  apreim  7703  mulge0  7719  divmuldivap  7800  divmul24ap  7804  divmuleqap  7805  recdivap  7806  divadddivap  7815  conjmulap  7817  prodgt0gt0  7929  ltmul12a  7938  lemul12b  7939  lediv2a  7973  qmulcl  8722  irrmul  8732  xrrege0  8892  ge0addcl  9004  ge0mulcl  9005  fzass4  9080  fzrev  9101  fzocatel  9208  serige0  9473  expclzaplem  9500  expge0  9512  expge1  9513  lt2sq  9549  le2sq  9550  bernneq  9593  sq11ap  9639  sqrt11ap  9924  2clim  10140  climge0  10163  opeo  10297  omeo  10298  cncongr1  10485