Theorem ad2ant2l 745

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 715	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 713	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  6642  mpteqb  7048  soxp  8170  wfrlem4OLD  8368  oaass  8617  nadd42  8755  naddel12  8756  undifixp  8992  undomOLD  9126  xpdom2  9133  tcrank  9953  inawinalem  10758  addcanpr  11115  ltsosr  11163  1re  11290  add42  11511  muladd  11722  mulsub  11733  divmuleq  11999  ltmul12a  12150  lemul12b  12151  lemul12a  12152  mulge0b  12165  qaddcl  13030  qmulcl  13032  iooshf  13486  fzass4  13622  elfzomelpfzo  13821  modid  13947  swrdccatin2  14777  pfxccatin12  14781  cshwleneq  14865  s2eq2seq  14986  tanaddlem  16214  fpwipodrs  18610  gsumsgrpccat  18875  issubg4  19185  ghmpreima  19278  cntzsubg  19379  symgfixf1  19479  rnghmsubcsetclem2  20654  rhmsubcsetclem2  20683  rhmsubcrngclem2  20689  islmodd  20886  lssvsubcl  20965  lssvscl  20976  lmhmf1o  21068  pwsdiaglmhm  21079  lmimco  21887  scmatghm  22560  scmatmhm  22561  mat2pmatscmxcl  22767  fctop  23032  cctop  23034  opnneissb  23143  pnrmopn  23372  hausnei2  23382  neitx  23636  txcnmpt  23653  txrest  23660  tx1stc  23679  fbssfi  23866  opnfbas  23871  rnelfmlem  23981  alexsubALTlem3  24078  metcnp3  24574  cncfmet  24954  evth  25010  caucfil  25336  ovolun  25553  dveflem  26037  efnnfsumcl  27164  efchtdvds  27220  lgsdir2  27392  precsexlem11  28259  axdimuniq  28946  axcontlem2  28998  clwwlkf1  30081  frgrwopreglem5lem  30352  frgrwopreglem5ALT  30354  friendship  30431  hvsub4  31069  his35  31120  shscli  31349  5oalem2  31687  3oalem2  31695  hosub4  31845  hmops  32052  hmopm  32053  hmopco  32055  adjmul  32124  adjadd  32125  mdslmd1lem1  32357  mdslmd1lem2  32358  satffunlem  35369  elmrsubrn  35488  dfon2lem6  35752  funline  36106  neibastop2lem  36326  isbasisrelowllem1  37321  isbasisrelowllem2  37322  mbfposadd  37627  itg2addnc  37634  fdc  37705  seqpo  37707  ismtyval  37760  paddss12  39776  zaddcom  42428  zmulcom  42432  mzpcompact2lem  42707  jm2.26  42959  orddif0suc  43230  tfsconcatun  43299  oaun3lem2  43337  fmtnofac2lem  47442  isubgrgrim  47781  zlmodzxzsubm  48084  ltsubaddb  48243  ltsubsubb  48244