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  7245  cocan1  7248  ordiso2  9444  fin1a2lem9  10337  fin1a2lem12  10340  gchpwdom  10599  winainflem  10622  bpolydif  15997  dvdsmodexp  16206  muldvds1  16226  lcmdvds  16554  ramcl  16976  oddvdsnn0  19450  ghmplusg  19752  frlmsslss2  21660  frlmsslsp  21681  islindf4  21723  mamures  22260  matepmcl  22325  matepm2cl  22326  pmatcollpw2lem  22640  cnpnei  23127  ssref  23375  qtopss  23578  elfm2  23811  flffbas  23858  cnpfcf  23904  deg1ldg  25973  brbtwn2  28808  colinearalg  28813  axsegconlem1  28820  upgrpredgv  29042  cusgrrusgr  29485  upgrewlkle2  29510  wwlksm1edg  29784  clwwlkf  29949  wwlksext2clwwlk  29959  nvmul0or  30552  hoadddi  31705  volfiniune  34193  bnj548  34860  funsseq  35728  nn0prpwlem  36283  fnemeet1  36327  curfv  37567  lindsadd  37580  keridl  37999  pmapglbx  39736  elpaddn0  39767  paddasslem9  39795  paddasslem10  39796  cdleme42mgN  40455  relexpxpmin  43679  ntrclsk3  44032  n0p  45012  wessf1ornlem  45152  infxr  45336  lptre2pt  45611  dvnprodlem1  45917  fourierdlem42  46120  fourierdlem48  46125  fourierdlem54  46131  fourierdlem77  46154  sge0rpcpnf  46392  hoicvr  46519  smflimsuplem7  46797