Theorem 3ad2antl3 1206

Description: Deduction adding conjuncts to antecedent. (Contributed by NM, 4-Aug-2007.)

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antl3

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantll 727	. 2 ⊢ (((𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1185	1 ⊢ (((𝜓 ∧ 𝜏 ∧ 𝜑) ∧ 𝜒) → 𝜃)

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl3  1212  simpl3l  1247  simpl3r  1248  simpl31  1273  simpl32  1274  simpl33  1275  rspc3ev  3596  brcogw  5851  cocan1  7309  ov6g  7594  fpr1  8335  onelfvnef1  8463  dif1enlem  9189  dif1ennnALT  9282  cfsmolem  10361  coftr  10364  axcc3  10529  axdc4lem  10546  gruf  10909  dedekindle  11487  zdivmul  12784  cshf1  14975  cshimadifsn  14994  fprodle  16178  bpolycl  16233  lcmdvds  16798  lubss  18702  odeq  19779  ghmplusg  20075  lmhmvsca  21335  islindf4  22159  lindsenlbs  22172  mndifsplit  22966  gsummatr01lem3  22987  gsummatr01  22989  mp2pm2mplem4  23142  elcls  23406  cnpresti  23621  cmpsublem  23732  comppfsc  23866  ptpjcn  23945  elfm3  24284  rnelfmlem  24286  nmoix  25063  caublcls  25645  ig1pdvds  26513  coeid3  26574  amgm  27333  brbtwn2  29498  colinearalg  29503  axsegconlem1  29510  ax5seglem1  29521  ax5seglem2  29522  homco1  32418  hoadddi  32420  scottrankeqel  35814  j0ltaleph  35965  jltaleph  35983  br6  36655  upixp  38809  filbcmb  38820  3dim1  40670  llni  40711  lplni  40735  lvoli  40778  cdleme42mgN  41691  mzprename  43906  infmrgelbi  44031  relexpxpmin  44863  n0p  46207  rexabslelem  46573  pimxrneun  46643  limcleqr  46799  fnlimfvre  46829  stoweidlem17  47172  stoweidlem28  47183  fourierdlem12  47274  fourierdlem41  47303  fourierdlem42  47304  fourierdlem74  47335  fourierdlem77  47338  qndenserrnopnlem  47452  issalnnd  47500  hspmbllem2  47782  issmfle  47900  smflimlem2  47927  smflimmpt  47965  smfinflem  47972  smflimsuplem7  47981  smflimsupmpt  47984  smfliminfmpt  47987  lighneallem3  48837