Theorem 3ad2antl2 1193

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

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

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 208  df-an 397  df-3an 1094

This theorem is referenced by:  simpl2  1199  simpl2l  1233  simpl2r  1234  simpl21  1258  simpl22  1259  simpl23  1260  fcofo  7232  cocan1  7235  ordiso2  9420  fin1a2lem9  10321  fin1a2lem12  10324  gchpwdom  10584  winainflem  10607  bpolydif  16011  dvdsmodexp  16220  muldvds1  16240  lcmdvds  16568  ramcl  16991  oddvdsnn0  19510  ghmplusg  19812  frlmsslss2  21750  frlmsslsp  21771  islindf4  21813  mamures  22380  matepmcl  22445  matepm2cl  22446  pmatcollpw2lem  22760  cnpnei  23247  ssref  23495  qtopss  23698  elfm2  23931  flffbas  23978  cnpfcf  24024  deg1ldg  26075  brbtwn2  28992  colinearalg  28997  axsegconlem1  29004  upgrpredgv  29226  cusgrrusgr  29668  upgrewlkle2  29693  wwlksm1edg  29967  clwwlkf  30135  wwlksext2clwwlk  30145  nvmul0or  30739  hoadddi  31892  volfiniune  34414  bnj548  35079  funsseq  35996  nn0prpwlem  36550  fnemeet1  36594  curfv  37967  lindsadd  37980  keridl  38399  pmapglbx  40261  elpaddn0  40292  paddasslem9  40320  paddasslem10  40321  cdleme42mgN  40980  relexpxpmin  44161  ntrclsk3  44514  n0p  45493  wessf1ornlem  45632  infxr  45811  lptre2pt  46083  dvnprodlem1  46389  fourierdlem42  46592  fourierdlem48  46597  fourierdlem54  46603  fourierdlem77  46626  sge0rpcpnf  46864  hoicvr  46991  smflimsuplem7  47269