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  6600  mpteqb  7005  soxp  8128  wfrlem4OLD  8326  oaass  8573  nadd42  8711  naddel12  8712  undifixp  8948  undomOLD  9074  xpdom2  9081  tcrank  9898  inawinalem  10703  addcanpr  11060  ltsosr  11108  1re  11235  add42  11457  muladd  11669  mulsub  11680  divmuleq  11946  ltmul12a  12097  lemul12b  12098  lemul12a  12099  mulge0b  12112  qaddcl  12981  qmulcl  12983  iooshf  13443  fzass4  13579  elfzomelpfzo  13787  modid  13913  swrdccatin2  14747  pfxccatin12  14751  cshwleneq  14835  s2eq2seq  14956  tanaddlem  16184  fpwipodrs  18550  gsumsgrpccat  18818  issubg4  19128  ghmpreima  19221  cntzsubg  19322  symgfixf1  19418  rnghmsubcsetclem2  20592  rhmsubcsetclem2  20621  rhmsubcrngclem2  20627  islmodd  20823  lssvsubcl  20901  lssvscl  20912  lmhmf1o  21004  pwsdiaglmhm  21015  lmimco  21804  scmatghm  22471  scmatmhm  22472  mat2pmatscmxcl  22678  fctop  22942  cctop  22944  opnneissb  23052  pnrmopn  23281  hausnei2  23291  neitx  23545  txcnmpt  23562  txrest  23569  tx1stc  23588  fbssfi  23775  opnfbas  23780  rnelfmlem  23890  alexsubALTlem3  23987  metcnp3  24479  cncfmet  24853  evth  24909  caucfil  25235  ovolun  25452  dveflem  25935  efnnfsumcl  27065  efchtdvds  27121  lgsdir2  27293  precsexlem11  28171  axdimuniq  28892  axcontlem2  28944  clwwlkf1  30030  frgrwopreglem5lem  30301  frgrwopreglem5ALT  30303  friendship  30380  hvsub4  31018  his35  31069  shscli  31298  5oalem2  31636  3oalem2  31644  hosub4  31794  hmops  32001  hmopm  32002  hmopco  32004  adjmul  32073  adjadd  32074  mdslmd1lem1  32306  mdslmd1lem2  32307  satffunlem  35423  elmrsubrn  35542  dfon2lem6  35806  funline  36160  neibastop2lem  36378  isbasisrelowllem1  37373  isbasisrelowllem2  37374  mbfposadd  37691  itg2addnc  37698  fdc  37769  seqpo  37771  ismtyval  37824  paddss12  39838  zaddcom  42495  zmulcom  42499  mzpcompact2lem  42774  jm2.26  43026  orddif0suc  43292  tfsconcatun  43361  oaun3lem2  43399  fmtnofac2lem  47582  isubgrgrim  47942  zlmodzxzsubm  48334  ltsubaddb  48490  ltsubsubb  48491