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  7263  cocan1  7266  ordiso2  9468  fin1a2lem9  10361  fin1a2lem12  10364  gchpwdom  10623  winainflem  10646  bpolydif  16021  dvdsmodexp  16230  muldvds1  16250  lcmdvds  16578  ramcl  17000  oddvdsnn0  19474  ghmplusg  19776  frlmsslss2  21684  frlmsslsp  21705  islindf4  21747  mamures  22284  matepmcl  22349  matepm2cl  22350  pmatcollpw2lem  22664  cnpnei  23151  ssref  23399  qtopss  23602  elfm2  23835  flffbas  23882  cnpfcf  23928  deg1ldg  25997  brbtwn2  28832  colinearalg  28837  axsegconlem1  28844  upgrpredgv  29066  cusgrrusgr  29509  upgrewlkle2  29534  wwlksm1edg  29811  clwwlkf  29976  wwlksext2clwwlk  29986  nvmul0or  30579  hoadddi  31732  volfiniune  34220  bnj548  34887  funsseq  35755  nn0prpwlem  36310  fnemeet1  36354  curfv  37594  lindsadd  37607  keridl  38026  pmapglbx  39763  elpaddn0  39794  paddasslem9  39822  paddasslem10  39823  cdleme42mgN  40482  relexpxpmin  43706  ntrclsk3  44059  n0p  45039  wessf1ornlem  45179  infxr  45363  lptre2pt  45638  dvnprodlem1  45944  fourierdlem42  46147  fourierdlem48  46152  fourierdlem54  46158  fourierdlem77  46181  sge0rpcpnf  46419  hoicvr  46546  smflimsuplem7  46824