Theorem ad2ant2l 746

Description: Deduction adding two conjuncts to antecedent. (Contributed by NM, 8-Jan-2006.)

Hypothesis

Ref	Expression
ad2ant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
ad2ant2l	⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Proof of Theorem ad2ant2l

Step	Hyp	Ref	Expression
1		ad2ant2.1	. . 3 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
2	1	adantrl 716	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 714	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 395

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

This theorem is referenced by:  funcnvqp  6541  mpteqb  6943  soxp  8054  oaass  8471  nadd42  8609  naddel12  8610  undifixp  8853  xpdom2  8980  tcrank  9769  inawinalem  10572  addcanpr  10929  ltsosr  10977  1re  11104  add42  11327  muladd  11541  mulsub  11552  divmuleq  11818  ltmul12a  11969  lemul12b  11970  lemul12a  11971  mulge0b  11984  qaddcl  12855  qmulcl  12857  iooshf  13318  fzass4  13454  elfzomelpfzo  13664  modid  13792  swrdccatin2  14628  pfxccatin12  14632  cshwleneq  14716  s2eq2seq  14836  tanaddlem  16067  fpwipodrs  18438  gsumsgrpccat  18740  issubg4  19050  ghmpreima  19143  cntzsubg  19244  symgfixf1  19342  rnghmsubcsetclem2  20540  rhmsubcsetclem2  20569  rhmsubcrngclem2  20575  islmodd  20792  lssvsubcl  20870  lssvscl  20881  lmhmf1o  20973  pwsdiaglmhm  20984  lmimco  21774  scmatghm  22441  scmatmhm  22442  mat2pmatscmxcl  22648  fctop  22912  cctop  22914  opnneissb  23022  pnrmopn  23251  hausnei2  23261  neitx  23515  txcnmpt  23532  txrest  23539  tx1stc  23558  fbssfi  23745  opnfbas  23750  rnelfmlem  23860  alexsubALTlem3  23957  metcnp3  24448  cncfmet  24822  evth  24878  caucfil  25203  ovolun  25420  dveflem  25903  efnnfsumcl  27033  efchtdvds  27089  lgsdir2  27261  precsexlem11  28148  axdimuniq  28884  axcontlem2  28936  clwwlkf1  30019  frgrwopreglem5lem  30290  frgrwopreglem5ALT  30292  friendship  30369  hvsub4  31007  his35  31058  shscli  31287  5oalem2  31625  3oalem2  31633  hosub4  31783  hmops  31990  hmopm  31991  hmopco  31993  adjmul  32062  adjadd  32063  mdslmd1lem1  32295  mdslmd1lem2  32296  satffunlem  35413  elmrsubrn  35532  dfon2lem6  35801  funline  36155  neibastop2lem  36373  isbasisrelowllem1  37368  isbasisrelowllem2  37369  mbfposadd  37686  itg2addnc  37693  fdc  37764  seqpo  37766  ismtyval  37819  paddss12  39837  zaddcom  42476  zmulcom  42480  mzpcompact2lem  42763  jm2.26  43014  orddif0suc  43280  tfsconcatun  43349  oaun3lem2  43387  fmtnofac2lem  47578  isubgrgrim  47939  zlmodzxzsubm  48369  ltsubaddb  48525  ltsubsubb  48526