Theorem ad2ant2l 744

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 714	. 2 ⊢ ((𝜑 ∧ (𝜏 ∧ 𝜓)) → 𝜒)
3	2	adantll 712	1 ⊢ (((𝜃 ∧ 𝜑) ∧ (𝜏 ∧ 𝜓)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 398

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 209  df-an 399

This theorem is referenced by:  funcnvqp  6421  mpteqb  6790  mpofun  7279  soxp  7826  wfrlem4  7961  oaass  8190  undifixp  8501  undom  8608  xpdom2  8615  tcrank  9316  inawinalem  10114  addcanpr  10471  ltsosr  10519  1re  10644  add42  10864  muladd  11075  mulsub  11086  divmuleq  11348  ltmul12a  11499  lemul12b  11500  lemul12a  11501  mulge0b  11513  qaddcl  12367  qmulcl  12369  iooshf  12818  fzass4  12948  elfzomelpfzo  13144  modid  13267  swrdccatin2  14094  pfxccatin12  14098  cshwleneq  14182  s2eq2seq  14302  tanaddlem  15522  fpwipodrs  17777  gsumsgrpccat  18007  issubg4  18301  ghmpreima  18383  cntzsubg  18470  symgfixf1  18568  islmodd  19643  lssvsubcl  19718  lssvscl  19730  lmhmf1o  19821  pwsdiaglmhm  19832  lmimco  20991  scmatghm  21145  scmatmhm  21146  mat2pmatscmxcl  21351  fctop  21615  cctop  21617  opnneissb  21725  pnrmopn  21954  hausnei2  21964  neitx  22218  txcnmpt  22235  txrest  22242  tx1stc  22261  fbssfi  22448  opnfbas  22453  rnelfmlem  22563  alexsubALTlem3  22660  metcnp3  23153  cncfmet  23519  evth  23566  caucfil  23889  ovolun  24103  dveflem  24579  efnnfsumcl  25683  efchtdvds  25739  lgsdir2  25909  axdimuniq  26702  axcontlem2  26754  clwwlkf1  27831  frgrwopreglem5lem  28102  frgrwopreglem5ALT  28104  friendship  28181  hvsub4  28817  his35  28868  shscli  29097  5oalem2  29435  3oalem2  29443  hosub4  29593  hmops  29800  hmopm  29801  hmopco  29803  adjmul  29872  adjadd  29873  mdslmd1lem1  30105  mdslmd1lem2  30106  satffunlem  32652  elmrsubrn  32771  dfon2lem6  33037  funline  33607  neibastop2lem  33712  isbasisrelowllem1  34640  isbasisrelowllem2  34641  mbfposadd  34943  itg2addnc  34950  fdc  35024  seqpo  35026  ismtyval  35082  paddss12  36959  mzpcompact2lem  39354  jm2.26  39605  fmtnofac2lem  43737  rnghmsubcsetclem2  44254  rhmsubcsetclem2  44300  rhmsubcrngclem2  44306  zlmodzxzsubm  44414  ltsubaddb  44576  ltsubsubb  44577