Theorem 3ad2antl2 1187

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 715	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1167	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 207  df-an 396  df-3an 1088

This theorem is referenced by:  simpl2  1193  simpl2l  1227  simpl2r  1228  simpl21  1252  simpl22  1253  simpl23  1254  fcofo  7286  cocan1  7289  ordiso2  9534  fin1a2lem9  10427  fin1a2lem12  10430  gchpwdom  10689  winainflem  10712  bpolydif  16076  dvdsmodexp  16285  muldvds1  16305  lcmdvds  16632  ramcl  17054  oddvdsnn0  19530  ghmplusg  19832  frlmsslss2  21740  frlmsslsp  21761  islindf4  21803  mamures  22340  matepmcl  22405  matepm2cl  22406  pmatcollpw2lem  22720  cnpnei  23207  ssref  23455  qtopss  23658  elfm2  23891  flffbas  23938  cnpfcf  23984  deg1ldg  26054  brbtwn2  28889  colinearalg  28894  axsegconlem1  28901  upgrpredgv  29123  cusgrrusgr  29566  upgrewlkle2  29591  wwlksm1edg  29868  clwwlkf  30033  wwlksext2clwwlk  30043  nvmul0or  30636  hoadddi  31789  volfiniune  34266  bnj548  34933  funsseq  35790  nn0prpwlem  36345  fnemeet1  36389  curfv  37629  lindsadd  37642  keridl  38061  pmapglbx  39793  elpaddn0  39824  paddasslem9  39852  paddasslem10  39853  cdleme42mgN  40512  relexpxpmin  43716  ntrclsk3  44069  n0p  45049  wessf1ornlem  45189  infxr  45374  lptre2pt  45649  dvnprodlem1  45955  fourierdlem42  46158  fourierdlem48  46163  fourierdlem54  46169  fourierdlem77  46192  sge0rpcpnf  46430  hoicvr  46557  smflimsuplem7  46835