Theorem 3ad2antl2 1188

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

Syntax hints:   → wi 4   ∧ wa 395   ∧ 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 207  df-an 396  df-3an 1089

This theorem is referenced by:  simpl2  1194  simpl2l  1228  simpl2r  1229  simpl21  1253  simpl22  1254  simpl23  1255  fcofo  7234  cocan1  7237  ordiso2  9421  fin1a2lem9  10319  fin1a2lem12  10322  gchpwdom  10582  winainflem  10605  bpolydif  16009  dvdsmodexp  16218  muldvds1  16238  lcmdvds  16566  ramcl  16989  oddvdsnn0  19508  ghmplusg  19810  frlmsslss2  21763  frlmsslsp  21784  islindf4  21826  mamures  22371  matepmcl  22436  matepm2cl  22437  pmatcollpw2lem  22751  cnpnei  23238  ssref  23486  qtopss  23689  elfm2  23922  flffbas  23969  cnpfcf  24015  deg1ldg  26069  brbtwn2  28993  colinearalg  28998  axsegconlem1  29005  upgrpredgv  29227  cusgrrusgr  29670  upgrewlkle2  29695  wwlksm1edg  29969  clwwlkf  30137  wwlksext2clwwlk  30147  nvmul0or  30741  hoadddi  31894  volfiniune  34395  bnj548  35060  funsseq  35971  nn0prpwlem  36525  fnemeet1  36569  curfv  37932  lindsadd  37945  keridl  38364  pmapglbx  40226  elpaddn0  40257  paddasslem9  40285  paddasslem10  40286  cdleme42mgN  40945  relexpxpmin  44159  ntrclsk3  44512  n0p  45491  wessf1ornlem  45630  infxr  45811  lptre2pt  46083  dvnprodlem1  46389  fourierdlem42  46592  fourierdlem48  46597  fourierdlem54  46603  fourierdlem77  46626  sge0rpcpnf  46864  hoicvr  46991  smflimsuplem7  47269