Theorem 3ad2antl2 1186

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 714	. 2 ⊢ (((𝜑 ∧ 𝜏) ∧ 𝜒) → 𝜃)
3	2	3adantl1 1166	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  1192  simpl2l  1226  simpl2r  1227  simpl21  1251  simpl22  1252  simpl23  1253  fcofo  7324  cocan1  7327  ordiso2  9584  fin1a2lem9  10477  fin1a2lem12  10480  gchpwdom  10739  winainflem  10762  bpolydif  16103  dvdsmodexp  16310  muldvds1  16329  lcmdvds  16655  ramcl  17076  oddvdsnn0  19586  ghmplusg  19888  frlmsslss2  21818  frlmsslsp  21839  islindf4  21881  mamures  22422  matepmcl  22489  matepm2cl  22490  pmatcollpw2lem  22804  cnpnei  23293  ssref  23541  qtopss  23744  elfm2  23977  flffbas  24024  cnpfcf  24070  deg1ldg  26151  brbtwn2  28938  colinearalg  28943  axsegconlem1  28950  upgrpredgv  29174  cusgrrusgr  29617  upgrewlkle2  29642  wwlksm1edg  29914  clwwlkf  30079  wwlksext2clwwlk  30089  nvmul0or  30682  hoadddi  31835  volfiniune  34194  bnj548  34873  funsseq  35731  nn0prpwlem  36288  fnemeet1  36332  curfv  37560  lindsadd  37573  keridl  37992  pmapglbx  39726  elpaddn0  39757  paddasslem9  39785  paddasslem10  39786  cdleme42mgN  40445  factwoffsmonot  42199  relexpxpmin  43679  ntrclsk3  44032  n0p  44945  wessf1ornlem  45092  infxr  45282  lptre2pt  45561  dvnprodlem1  45867  fourierdlem42  46070  fourierdlem48  46075  fourierdlem54  46081  fourierdlem77  46104  sge0rpcpnf  46342  hoicvr  46469  smflimsuplem7  46747