Theorem 3ad2antl2 1205

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401   ∧ w3a 1103

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402  df-3an 1105

This theorem is used by:  simpl2  1211  simpl2l  1245  simpl2r  1246  simpl21  1270  simpl22  1271  simpl23  1272  fcofo  7296  cocan1  7299  onelfvnef1  8449  curfv  8892  ordiso2  9509  fin1a2lem9  10486  fin1a2lem12  10489  gchpwdom  10755  winainflem  10778  bpolydif  16221  dvdsmodexp  16430  muldvds1  16450  lcmdvds  16783  ramcl  17207  oddvdsnn0  19758  ghmplusg  20060  frlmsslss2  22081  frlmsslsp  22102  islindf4  22144  mamures  22712  matepmcl  22777  matepm2cl  22778  pmatcollpw2lem  23095  cnpnei  23582  ssref  23831  qtopss  24034  elfm2  24267  flffbas  24314  cnpfcf  24360  deg1ldg  26410  brbtwn2  29483  colinearalg  29488  axsegconlem1  29495  upgrpredgv  29717  cusgrrusgr  30162  upgrewlkle2  30187  wwlksm1edg  30470  clwwlkf  30638  wwlksext2clwwlk  30648  nvmul0or  31252  hoadddi  32405  volfiniune  34905  bnj548  35569  funsseq  36575  nn0prpwlem  37152  fnemeet1  37196  lindsadd  38579  keridl  39009  pmapglbx  40869  elpaddn0  40900  paddasslem9  40928  paddasslem10  40929  cdleme42mgN  41588  relexpxpmin  44759  ntrclsk3  45112  n0p  46104  wessf1ornlem  46242  infxr  46420  lptre2pt  46692  dvnprodlem1  46998  fourierdlem42  47201  fourierdlem48  47206  fourierdlem54  47212  fourierdlem77  47235  sge0rpcpnf  47473  hoicvr  47600  smflimsuplem7  47878