Theorem 3ad2ant2 926

Description: Deduction adding conjuncts to an antecedent. (Contributed by NM, 21-Apr-2005.)

Hypothesis

Ref	Expression
3ad2ant.1	⊢ (𝜑 → 𝜒)

Assertion

Ref	Expression
3ad2ant2	⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Proof of Theorem 3ad2ant2

Step	Hyp	Ref	Expression
1		3ad2ant.1	. . 3 ⊢ (𝜑 → 𝜒)
2	1	adantr 261	. 2 ⊢ ((𝜑 ∧ 𝜃) → 𝜒)
3	2	3adant1 922	1 ⊢ ((𝜓 ∧ 𝜑 ∧ 𝜃) → 𝜒)

Syntax hints:   → wi 4   ∧ w3a 885

This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-mp 7  ax-ia1 99  ax-ia2 100  ax-ia3 101

This theorem depends on definitions:  df-bi 110  df-3an 887

This theorem is referenced by:  simp2l  930  simp2r  931  simp21  937  simp22  938  simp23  939  simp2ll  971  simp2lr  972  simp2rl  973  simp2rr  974  simp2l1  1003  simp2l2  1004  simp2l3  1005  simp2r1  1006  simp2r2  1007  simp2r3  1008  simp21l  1021  simp21r  1022  simp22l  1023  simp22r  1024  simp23l  1025  simp23r  1026  simp211  1042  simp212  1043  simp213  1044  simp221  1045  simp222  1046  simp223  1047  simp231  1048  simp232  1049  simp233  1050  3anim123i  1089  3jaao  1203  ceqsalt  2580  vtoclgft  2604  vtoclegft  2625  ifbothdc  3357  frirrg  4087  elirr  4266  en2lp  4278  reg3exmidlemwe  4303  sotri3  4723  funtpg  4950  fnprg  4954  fntpg  4955  funimaexglem  4982  fnco  5007  fvun1  5239  oprssov  5642  caovimo  5694  rdgivallem  5968  f1dom2g  6236  ordiso2  6357  distrnqg  6485  distrnq0  6557  prarloclem5  6598  cauappcvgprlemlol  6745  cauappcvgprlemupu  6747  caucvgprlemlol  6768  caucvgprlemupu  6770  caucvgprprlemlol  6796  caucvgprprlemupu  6798  cnegexlem2  7187  apcotr  7598  apadd1  7599  mulext1  7603  div2negap  7711  ltdiv2  7853  nndivtr  7955  zdivmul  8330  gtndiv  8335  fzind  8353  eluzuzle  8481  eluzp1p1  8498  peano2uz  8526  qdivcl  8577  irrmul  8581  ledivge1le  8652  xrre2  8734  ubioc1  8798  ubicc2  8853  uzsubsubfz  8911  elfz1b  8952  fzp1nel  8966  fz0fzdiffz0  8987  difelfzle  8992  elfzo0  9038  elfzonlteqm1  9066  fzonn0p1p1  9069  fzosplitprm1  9090  fzoshftral  9094  subfzo0  9097  ceiqle  9155  modqval  9166  modqvalr  9167  flqpmodeq  9169  modq0  9171  mulqmod0  9172  negqmod0  9173  modqge0  9174  modqlt  9175  modqelico  9176  modqdiffl  9177  modqmulnn  9184  expival  9257  redivap  9474  imdivap  9481  climuni  9814  mulcn2  9833