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 399

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 210  df-an 400

This theorem is referenced by:  funcnvqp  6403  mpteqb  6794  mpofunOLD  7291  soxp  7849  wfrlem4  7987  oaass  8218  undifixp  8544  undom  8654  xpdom2  8661  tcrank  9386  inawinalem  10189  addcanpr  10546  ltsosr  10594  1re  10719  add42  10939  muladd  11150  mulsub  11161  divmuleq  11423  ltmul12a  11574  lemul12b  11575  lemul12a  11576  mulge0b  11588  qaddcl  12447  qmulcl  12449  iooshf  12900  fzass4  13036  elfzomelpfzo  13232  modid  13355  swrdccatin2  14180  pfxccatin12  14184  cshwleneq  14268  s2eq2seq  14388  tanaddlem  15611  fpwipodrs  17890  gsumsgrpccat  18120  issubg4  18416  ghmpreima  18498  cntzsubg  18585  symgfixf1  18683  islmodd  19759  lssvsubcl  19834  lssvscl  19846  lmhmf1o  19937  pwsdiaglmhm  19948  lmimco  20660  scmatghm  21284  scmatmhm  21285  mat2pmatscmxcl  21491  fctop  21755  cctop  21757  opnneissb  21865  pnrmopn  22094  hausnei2  22104  neitx  22358  txcnmpt  22375  txrest  22382  tx1stc  22401  fbssfi  22588  opnfbas  22593  rnelfmlem  22703  alexsubALTlem3  22800  metcnp3  23293  cncfmet  23661  evth  23711  caucfil  24035  ovolun  24251  dveflem  24731  efnnfsumcl  25840  efchtdvds  25896  lgsdir2  26066  axdimuniq  26859  axcontlem2  26911  clwwlkf1  27986  frgrwopreglem5lem  28257  frgrwopreglem5ALT  28259  friendship  28336  hvsub4  28972  his35  29023  shscli  29252  5oalem2  29590  3oalem2  29598  hosub4  29748  hmops  29955  hmopm  29956  hmopco  29958  adjmul  30027  adjadd  30028  mdslmd1lem1  30260  mdslmd1lem2  30261  satffunlem  32934  elmrsubrn  33053  dfon2lem6  33336  funline  34082  neibastop2lem  34187  isbasisrelowllem1  35149  isbasisrelowllem2  35150  mbfposadd  35447  itg2addnc  35454  fdc  35526  seqpo  35528  ismtyval  35581  paddss12  37456  mzpcompact2lem  40145  jm2.26  40396  fmtnofac2lem  44554  rnghmsubcsetclem2  45068  rhmsubcsetclem2  45114  rhmsubcrngclem2  45120  zlmodzxzsubm  45229  ltsubaddb  45389  ltsubsubb  45390