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  7222  cocan1  7225  ordiso2  9401  fin1a2lem9  10299  fin1a2lem12  10302  gchpwdom  10561  winainflem  10584  bpolydif  15962  dvdsmodexp  16171  muldvds1  16191  lcmdvds  16519  ramcl  16941  oddvdsnn0  19456  ghmplusg  19758  frlmsslss2  21712  frlmsslsp  21733  islindf4  21775  mamures  22312  matepmcl  22377  matepm2cl  22378  pmatcollpw2lem  22692  cnpnei  23179  ssref  23427  qtopss  23630  elfm2  23863  flffbas  23910  cnpfcf  23956  deg1ldg  26024  brbtwn2  28883  colinearalg  28888  axsegconlem1  28895  upgrpredgv  29117  cusgrrusgr  29560  upgrewlkle2  29585  wwlksm1edg  29859  clwwlkf  30027  wwlksext2clwwlk  30037  nvmul0or  30630  hoadddi  31783  volfiniune  34243  bnj548  34909  funsseq  35812  nn0prpwlem  36364  fnemeet1  36408  curfv  37648  lindsadd  37661  keridl  38080  pmapglbx  39816  elpaddn0  39847  paddasslem9  39875  paddasslem10  39876  cdleme42mgN  40535  relexpxpmin  43758  ntrclsk3  44111  n0p  45090  wessf1ornlem  45230  infxr  45413  lptre2pt  45686  dvnprodlem1  45992  fourierdlem42  46195  fourierdlem48  46200  fourierdlem54  46206  fourierdlem77  46229  sge0rpcpnf  46467  hoicvr  46594  smflimsuplem7  46872