Theorem 3adant3r 1315

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

Hypothesis

Ref	Expression
3adant1l.1	⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)

Assertion

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

Proof of Theorem 3adant3r

Step	Hyp	Ref	Expression
1		3adant1l.1	. . . 4 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3com13 1262	. . 3 ⊢ ((𝜒 ∧ 𝜓 ∧ 𝜑) → 𝜃)
3	2	3adant1r 1311	. 2 ⊢ (((𝜒 ∧ 𝜏) ∧ 𝜓 ∧ 𝜑) → 𝜃)
4	3	3com13 1262	1 ⊢ ((𝜑 ∧ 𝜓 ∧ (𝜒 ∧ 𝜏)) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 383   ∧ w3a 1031

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 196  df-an 385  df-3an 1033

This theorem is referenced by:  wfrlem12  7313  mapfien2  8197  cfeq0  8961  ltmul2  10753  lemul1  10754  lemul2  10755  lemuldiv  10782  lediv2  10792  ltdiv23  10793  lediv23  10794  dvdscmulr  14848  dvdsmulcr  14849  modremain  14970  ndvdsadd  14972  rpexp12i  15272  isdrngd  18595  cramerimp  20311  tsmsxp  21768  xblcntrps  22025  xblcntr  22026  rrxmet  22999  nvaddsub4  26896  hvmulcan2  27314  adjlnop  28329  frrlem11  31036  rrnmet  32798  lfladd  33371  lflsub  33372  lshpset2N  33424  atcvrj1  33735  athgt  33760  ltrncnvel  34446  trlcnv  34470  trljat2  34472  cdlemc5  34500  trlcoabs  35027  trlcolem  35032  dicvaddcl  35497  fourierdlem42  39042  ovnhoilem2  39492  lincext3  42039