Theorem 3ad2antl2 1186

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

Hypothesis

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

Assertion

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

Proof of Theorem 3ad2antl2

Step	Hyp	Ref	Expression
1		3ad2antl.1	. . 3 ⊢ ((𝜑 ∧ 𝜒) → 𝜃)
2	1	adantlr 713	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1166	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 396   ∧ w3a 1087

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 206  df-an 397  df-3an 1089

This theorem is referenced by:  simpl2  1192  simpl2l  1226  simpl2r  1227  simpl21  1251  simpl22  1252  simpl23  1253  fcofo  7239  cocan1  7242  ordiso2  9460  fin1a2lem9  10353  fin1a2lem12  10356  gchpwdom  10615  winainflem  10638  bpolydif  15949  dvdsmodexp  16155  muldvds1  16174  lcmdvds  16495  ramcl  16912  oddvdsnn0  19340  ghmplusg  19638  frlmsslss2  21218  frlmsslsp  21239  islindf4  21281  mamures  21776  matepmcl  21848  matepm2cl  21849  pmatcollpw2lem  22163  cnpnei  22652  ssref  22900  qtopss  23103  elfm2  23336  flffbas  23383  cnpfcf  23429  deg1ldg  25494  brbtwn2  27917  colinearalg  27922  axsegconlem1  27929  upgrpredgv  28153  cusgrrusgr  28592  upgrewlkle2  28617  wwlksm1edg  28889  clwwlkf  29054  wwlksext2clwwlk  29064  nvmul0or  29655  hoadddi  30808  volfiniune  32918  bnj548  33598  funsseq  34428  nn0prpwlem  34870  fnemeet1  34914  curfv  36131  lindsadd  36144  keridl  36564  pmapglbx  38305  elpaddn0  38336  paddasslem9  38364  paddasslem10  38365  cdleme42mgN  39024  factwoffsmonot  40688  relexpxpmin  42111  ntrclsk3  42464  n0p  43373  wessf1ornlem  43525  infxr  43722  lptre2pt  44001  dvnprodlem1  44307  fourierdlem42  44510  fourierdlem48  44515  fourierdlem54  44521  fourierdlem77  44544  sge0rpcpnf  44782  hoicvr  44909  smflimsuplem7  45187  isomgrsym  46148