Theorem adantrr 479

Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 4-May-1994.) (Proof shortened by Wolf Lammen, 24-Nov-2012.)

Hypothesis

Ref	Expression
adant2.1	⊢ ((𝜑 ∧ 𝜓) → 𝜒)

Assertion

Ref	Expression
adantrr	⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Proof of Theorem adantrr

Step	Hyp	Ref	Expression
1		simpl 109	. 2 ⊢ ((𝜓 ∧ 𝜃) → 𝜓)
2		adant2.1	. 2 ⊢ ((𝜑 ∧ 𝜓) → 𝜒)
3	1, 2	sylan2 286	1 ⊢ ((𝜑 ∧ (𝜓 ∧ 𝜃)) → 𝜒)

Syntax hints:   → wi 4   ∧ wa 104

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 106  ax-ia2 107  ax-ia3 108

This theorem is referenced by:  ad2ant2r  509  ad2ant2lr  510  dn1dc  962  3ad2antr1  1164  xordidc  1410  po2nr  4327  sotricim  4341  fmptco  5703  fvtp1g  5745  dff13  5790  fcof1o  5811  isocnv  5833  isores2  5835  isoini  5840  f1oiso2  5849  acexmidlemab  5891  ovmpodf  6029  offval  6115  xp1st  6191  1stconst  6247  cnvf1olem  6250  f1od2  6261  mpoxopoveq  6266  nnaordi  6534  nnmordi  6542  erinxp  6636  dom2lem  6799  fundmen  6833  pw2f1odclem  6863  mapen  6875  ssenen  6880  fidifsnen  6899  difinfsnlem  7129  fodjum  7175  cc2lem  7296  ltsonq  7428  lt2addnq  7434  lt2mulnq  7435  ltexnqq  7438  prarloclemarch2  7449  enq0sym  7462  genprndl  7551  genprndu  7552  prmuloc  7596  distrlem1prl  7612  distrlem1pru  7613  ltsopr  7626  ltexprlemdisj  7636  ltexprlemfl  7639  ltexprlemfu  7641  addcanprlemu  7645  ltaprg  7649  mulcmpblnrlemg  7770  recexgt0sr  7803  mul4  8120  2addsub  8202  muladd  8372  ltleadd  8434  eqord1  8471  eqord2  8472  divmulap3  8665  divcanap7  8709  divadddivap  8715  lemul2a  8847  lemul12b  8849  ltmuldiv2  8863  ltdivmul  8864  ltdivmul2  8866  ledivmul2  8868  lemuldiv2  8870  lt2msq  8874  cju  8949  zextlt  9376  xrlttr  9827  xrre3  9854  ixxdisj  9935  iooshf  9984  icodisj  10024  iccf1o  10036  expsubap  10602  bcval5  10778  hashfacen  10851  seq3coll  10857  sqrt0rlem  11047  lenegsq  11139  zsumdc  11427  fisum0diag2  11490  prodmodclem2  11620  zproddc  11622  ndvdsadd  11971  zssinfcl  11984  lcmdvds  12114  oddpwdclemdc  12208  hashdvds  12256  phisum  12275  pcqmul  12338  pcmpt  12378  4sqlemffi  12431  4sqlem11  12436  ennnfonelemex  12468  grpinvid1  13011  grpinvid2  13012  grplcan  13021  grpnpncan0  13055  dfgrp3mlem  13057  dfgrp3m  13058  grplactcnv  13061  0nsg  13170  eqger  13180  resghm  13216  conjghm  13232  eltg2  14030  ssnei2  14134  restopnb  14158  txdis1cn  14255  txlm  14256  elbl2ps  14369  elbl2  14370  blininf  14401  xmeter  14413  xmetresbl  14417  bdxmet  14478  metrest  14483  dedekindicc  14588  limcimo  14611