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 206  df-an 396

This theorem is referenced by:  funcnvqp  6617  mpteqb  7024  mpofunOLD  7545  soxp  8134  wfrlem4OLD  8333  oaass  8582  nadd42  8720  naddel12  8721  undifixp  8953  undomOLD  9085  xpdom2  9092  tcrank  9908  inawinalem  10713  addcanpr  11070  ltsosr  11118  1re  11245  add42  11466  muladd  11677  mulsub  11688  divmuleq  11950  ltmul12a  12101  lemul12b  12102  lemul12a  12103  mulge0b  12115  qaddcl  12980  qmulcl  12982  iooshf  13436  fzass4  13572  elfzomelpfzo  13769  modid  13894  swrdccatin2  14712  pfxccatin12  14716  cshwleneq  14800  s2eq2seq  14921  tanaddlem  16143  fpwipodrs  18532  gsumsgrpccat  18792  issubg4  19100  ghmpreima  19192  cntzsubg  19290  symgfixf1  19392  rnghmsubcsetclem2  20565  rhmsubcsetclem2  20594  rhmsubcrngclem2  20600  islmodd  20749  lssvsubcl  20828  lssvscl  20839  lmhmf1o  20931  pwsdiaglmhm  20942  lmimco  21778  scmatghm  22448  scmatmhm  22449  mat2pmatscmxcl  22655  fctop  22920  cctop  22922  opnneissb  23031  pnrmopn  23260  hausnei2  23270  neitx  23524  txcnmpt  23541  txrest  23548  tx1stc  23567  fbssfi  23754  opnfbas  23759  rnelfmlem  23869  alexsubALTlem3  23966  metcnp3  24462  cncfmet  24842  evth  24898  caucfil  25224  ovolun  25441  dveflem  25924  efnnfsumcl  27048  efchtdvds  27104  lgsdir2  27276  precsexlem11  28128  axdimuniq  28737  axcontlem2  28789  clwwlkf1  29872  frgrwopreglem5lem  30143  frgrwopreglem5ALT  30145  friendship  30222  hvsub4  30860  his35  30911  shscli  31140  5oalem2  31478  3oalem2  31486  hosub4  31636  hmops  31843  hmopm  31844  hmopco  31846  adjmul  31915  adjadd  31916  mdslmd1lem1  32148  mdslmd1lem2  32149  satffunlem  35011  elmrsubrn  35130  dfon2lem6  35384  funline  35738  neibastop2lem  35844  isbasisrelowllem1  36834  isbasisrelowllem2  36835  mbfposadd  37140  itg2addnc  37147  fdc  37218  seqpo  37220  ismtyval  37273  paddss12  39292  zaddcom  42007  zmulcom  42011  mzpcompact2lem  42171  jm2.26  42423  orddif0suc  42697  tfsconcatun  42766  oaun3lem2  42804  fmtnofac2lem  46908  zlmodzxzsubm  47423  ltsubaddb  47582  ltsubsubb  47583