Theorem 3ad2antl2 1203

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

Syntax hints:   → wi 4   ∧ wa 400   ∧ w3a 1101

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 210  df-an 401  df-3an 1103

This theorem is referenced by:  simpl2  1209  simpl2l  1243  simpl2r  1244  simpl21  1268  simpl22  1269  simpl23  1270  fcofo  7287  cocan1  7290  ordiso2  9476  fin1a2lem9  10391  fin1a2lem12  10394  gchpwdom  10654  winainflem  10677  bpolydif  16108  dvdsmodexp  16317  muldvds1  16337  lcmdvds  16665  ramcl  17088  oddvdsnn0  19613  ghmplusg  19915  frlmsslss2  21893  frlmsslsp  21914  islindf4  21956  mamures  22522  matepmcl  22587  matepm2cl  22588  pmatcollpw2lem  22902  cnpnei  23389  ssref  23637  qtopss  23840  elfm2  24073  flffbas  24120  cnpfcf  24166  deg1ldg  26217  brbtwn2  29195  colinearalg  29200  axsegconlem1  29207  upgrpredgv  29429  cusgrrusgr  29871  upgrewlkle2  29896  wwlksm1edg  30170  clwwlkf  30338  wwlksext2clwwlk  30348  nvmul0or  30942  hoadddi  32095  volfiniune  34564  bnj548  35229  funsseq  36158  nn0prpwlem  36721  fnemeet1  36765  curfv  38138  lindsadd  38151  keridl  38570  pmapglbx  40432  elpaddn0  40463  paddasslem9  40491  paddasslem10  40492  cdleme42mgN  41151  relexpxpmin  44334  ntrclsk3  44687  n0p  45656  wessf1ornlem  45794  infxr  45973  lptre2pt  46245  dvnprodlem1  46551  fourierdlem42  46754  fourierdlem48  46759  fourierdlem54  46765  fourierdlem77  46788  sge0rpcpnf  47026  hoicvr  47153  smflimsuplem7  47431