Theorem 3adant3r1 1266

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 16-Feb-2008.)

Hypothesis

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

Assertion

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

Proof of Theorem 3adant3r1

Step	Hyp	Ref	Expression
1		3exp.1	. . 3 ⊢ ((𝜑 ∧ 𝜓 ∧ 𝜒) → 𝜃)
2	1	3expb 1258	. 2 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜒)) → 𝜃)
3	2	3adantr1 1213	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:  plttr  16793  pltletr  16794  latjlej1  16888  latjlej2  16889  latnlej  16891  latnlej2  16894  latmlem2  16905  latledi  16912  latjass  16918  latj32  16920  latj13  16921  ipopos  16983  tsrlemax  17043  imasmnd2  17150  grpsubsub  17327  grpnnncan2  17335  imasgrp2  17353  mulgnn0ass  17401  mulgsubdir  17405  cmn32  18034  ablsubadd  18040  imasring  18442  zntoslem  19724  xmettri3  21968  mettri3  21969  xmetrtri  21970  xmetrtri2  21971  metrtri  21972  cphdivcl  22790  cphassr  22820  relogbmulexp  24316  grpodivdiv  26778  grpomuldivass  26779  ablo32  26787  ablodivdiv4  26792  ablodiv32  26793  ablonnncan  26794  nvmdi  26887  dipdi  27082  dipassr  27085  dipsubdir  27087  dipsubdi  27088  dvrcan5  29124  cgr3tr4  31329  cgr3rflx  31331  endofsegid  31362  seglemin  31390  broutsideof2  31399  rngosubdi  32914  rngosubdir  32915  isdrngo2  32927  crngm23  32971  dmncan2  33046  latmassOLD  33534  latm32  33536  cvrnbtwn4  33584  cvrcmp2  33589  ltcvrntr  33728  atcvrj0  33732  3dim3  33773  paddasslem17  34140  paddass  34142  lautlt  34395  lautcvr  34396  lautj  34397  lautm  34398  erngdvlem3  35296  dvalveclem  35332  mendlmod  36782  upgr1wlkvtxedg  40853