Theorem 3ad2antl2 1185

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 712	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1165	1 ⊢ (((𝜓 ∧ 𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)

Syntax hints:   → wi 4   ∧ wa 395   ∧ w3a 1086

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 396  df-3an 1088

This theorem is referenced by:  simpl2  1191  simpl2l  1225  simpl2r  1226  simpl21  1250  simpl22  1251  simpl23  1252  fcofo  7289  cocan1  7292  ordiso2  9514  fin1a2lem9  10407  fin1a2lem12  10410  gchpwdom  10669  winainflem  10692  bpolydif  16004  dvdsmodexp  16210  muldvds1  16229  lcmdvds  16550  ramcl  16967  oddvdsnn0  19454  ghmplusg  19756  frlmsslss2  21550  frlmsslsp  21571  islindf4  21613  mamures  22113  matepmcl  22185  matepm2cl  22186  pmatcollpw2lem  22500  cnpnei  22989  ssref  23237  qtopss  23440  elfm2  23673  flffbas  23720  cnpfcf  23766  deg1ldg  25846  brbtwn2  28431  colinearalg  28436  axsegconlem1  28443  upgrpredgv  28667  cusgrrusgr  29106  upgrewlkle2  29131  wwlksm1edg  29403  clwwlkf  29568  wwlksext2clwwlk  29578  nvmul0or  30171  hoadddi  31324  volfiniune  33527  bnj548  34207  funsseq  35044  nn0prpwlem  35511  fnemeet1  35555  curfv  36772  lindsadd  36785  keridl  37204  pmapglbx  38944  elpaddn0  38975  paddasslem9  39003  paddasslem10  39004  cdleme42mgN  39663  factwoffsmonot  41330  relexpxpmin  42771  ntrclsk3  43124  n0p  44032  wessf1ornlem  44183  infxr  44376  lptre2pt  44655  dvnprodlem1  44961  fourierdlem42  45164  fourierdlem48  45169  fourierdlem54  45175  fourierdlem77  45198  sge0rpcpnf  45436  hoicvr  45563  smflimsuplem7  45841  isomgrsym  46803