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  7236  cocan1  7239  ordiso2  9423  fin1a2lem9  10321  fin1a2lem12  10324  gchpwdom  10584  winainflem  10607  bpolydif  16011  dvdsmodexp  16220  muldvds1  16240  lcmdvds  16568  ramcl  16991  oddvdsnn0  19510  ghmplusg  19812  frlmsslss2  21765  frlmsslsp  21786  islindf4  21828  mamures  22372  matepmcl  22437  matepm2cl  22438  pmatcollpw2lem  22752  cnpnei  23239  ssref  23487  qtopss  23690  elfm2  23923  flffbas  23970  cnpfcf  24016  deg1ldg  26067  brbtwn2  28988  colinearalg  28993  axsegconlem1  29000  upgrpredgv  29222  cusgrrusgr  29665  upgrewlkle2  29690  wwlksm1edg  29964  clwwlkf  30132  wwlksext2clwwlk  30142  nvmul0or  30736  hoadddi  31889  volfiniune  34390  bnj548  35055  funsseq  35966  nn0prpwlem  36520  fnemeet1  36564  curfv  37935  lindsadd  37948  keridl  38367  pmapglbx  40229  elpaddn0  40260  paddasslem9  40288  paddasslem10  40289  cdleme42mgN  40948  relexpxpmin  44162  ntrclsk3  44515  n0p  45494  wessf1ornlem  45633  infxr  45814  lptre2pt  46086  dvnprodlem1  46392  fourierdlem42  46595  fourierdlem48  46600  fourierdlem54  46606  fourierdlem77  46629  sge0rpcpnf  46867  hoicvr  46994  smflimsuplem7  47272