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  6554  mpteqb  6958  soxp  8069  oaass  8486  nadd42  8625  naddel12  8626  undifixp  8870  xpdom2  8998  tcrank  9794  inawinalem  10598  addcanpr  10955  ltsosr  11003  1re  11130  add42  11353  muladd  11567  mulsub  11578  divmuleq  11844  ltmul12a  11995  lemul12b  11996  lemul12a  11997  mulge0b  12010  qaddcl  12876  qmulcl  12878  iooshf  13340  fzass4  13476  elfzomelpfzo  13686  modid  13814  swrdccatin2  14650  pfxccatin12  14654  cshwleneq  14738  s2eq2seq  14858  tanaddlem  16089  fpwipodrs  18461  gsumsgrpccat  18763  issubg4  19073  ghmpreima  19165  cntzsubg  19266  symgfixf1  19364  rnghmsubcsetclem2  20563  rhmsubcsetclem2  20592  rhmsubcrngclem2  20598  islmodd  20815  lssvsubcl  20893  lssvscl  20904  lmhmf1o  20996  pwsdiaglmhm  21007  lmimco  21797  scmatghm  22475  scmatmhm  22476  mat2pmatscmxcl  22682  fctop  22946  cctop  22948  opnneissb  23056  pnrmopn  23285  hausnei2  23295  neitx  23549  txcnmpt  23566  txrest  23573  tx1stc  23592  fbssfi  23779  opnfbas  23784  rnelfmlem  23894  alexsubALTlem3  23991  metcnp3  24482  cncfmet  24856  evth  24912  caucfil  25237  ovolun  25454  dveflem  25937  efnnfsumcl  27067  efchtdvds  27123  lgsdir2  27295  precsexlem11  28185  axdimuniq  28935  axcontlem2  28987  clwwlkf1  30073  frgrwopreglem5lem  30344  frgrwopreglem5ALT  30346  friendship  30423  hvsub4  31061  his35  31112  shscli  31341  5oalem2  31679  3oalem2  31687  hosub4  31837  hmops  32044  hmopm  32045  hmopco  32047  adjmul  32116  adjadd  32117  mdslmd1lem1  32349  mdslmd1lem2  32350  noinfepfnregs  35237  satffunlem  35544  elmrsubrn  35663  dfon2lem6  35929  funline  36285  neibastop2lem  36503  isbasisrelowllem1  37499  isbasisrelowllem2  37500  mbfposadd  37807  itg2addnc  37814  fdc  37885  seqpo  37887  ismtyval  37940  paddss12  40018  zaddcom  42661  zmulcom  42665  mzpcompact2lem  42935  jm2.26  43186  orddif0suc  43452  tfsconcatun  43521  oaun3lem2  43559  fmtnofac2lem  47756  isubgrgrim  48117  zlmodzxzsubm  48547  ltsubaddb  48702  ltsubsubb  48703