Theorem ad2ant2l 759

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

This proof depends on syntax axioms:   → wi 4   ∧ wa 401

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-an 402

This theorem is used by:  funcnvqp  6634  mpteqb  7044  soxp  8178  oaass  8607  nadd42  8747  naddel12  8748  undifixp  9000  xpdom2  9129  tcrank  9938  elhf3OLD  9960  inawinalem  10813  addcanpr  11170  ltsosr  11218  1re  11347  add42  11571  muladd  11787  mulsub  11798  divmuleq  12062  ltmul12a  12213  lemul12b  12214  lemul12a  12215  mulge0b  12227  qaddcl  13133  qmulcl  13135  iooshf  13597  fzass4  13736  elfzomelpfzo  13947  modid  14076  swrdccatin2  14920  pfxccatin12  14924  cshwleneq  15010  s2eq2seq  15131  tanaddlem  16378  fpwipodrs  18764  gsumsgrpccat  19086  issubg4  19406  ghmpreima  19502  cntzsubg  19604  symgfixf1  19702  rnghmsubcsetclem2  20935  rhmsubcsetclem2  20964  rhmsubcrngclem2  20970  islmodd  21192  lssvsubcl  21270  lssvscl  21281  lmhmf1o  21372  pwsdiaglmhm  21383  lmimco  22205  scmatghm  22903  scmatmhm  22904  mat2pmatscmxcl  23113  fctop  23377  cctop  23379  opnneissb  23487  pnrmopn  23716  hausnei2  23726  neitx  23981  txcnmpt  23998  txrest  24005  tx1stc  24024  fbssfi  24211  opnfbas  24216  rnelfmlem  24326  alexsubALTlem3  24423  metcnp3  24914  cncfmet  25285  evth  25335  caucfil  25659  ovolun  25875  dveflem  26354  efnnfsumcl  27487  efchtdvds  27543  lgsdir2  27714  precsexlem11  28660  axdimuniq  29548  axcontlem2  29600  clwwlkf1  30697  frgrwopreglem5lem  30978  frgrwopreglem5ALT  30980  friendship  31057  hvsub4  31696  his35  31747  shscli  31976  5oalem2  32314  3oalem2  32322  hosub4  32472  hmops  32679  hmopm  32680  hmopco  32682  adjmul  32751  adjadd  32752  mdslmd1lem1  32984  mdslmd1lem2  32985  noinfepfnregs  35941  satffunlem  36374  elmrsubrn  36493  dfon2lem6  36765  funline  37122  nmulprop  37154  nmulel1  37179  neibastop2lem  37363  isbasisrelowllem1  38546  isbasisrelowllem2  38547  mbfposadd  38853  itg2addnc  38860  fdc  38945  seqpo  38947  ismtyval  39000  paddss12  41142  zaddcom  43794  zmulcom  43798  mzpcompact2lem  44028  jm2.26  44275  orddif0suc  44531  tfsconcatun  44600  oaun3lem2  44638  fmtnofac2lem  48926  isubgrgrim  49300  lazmulzcl  49737  zlmodzxzsubm  49802  ltsubaddb  49957  ltsubsubb  49958