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  968  3ad2antr1  1188  xordidc  1443  po2nr  4406  sotricim  4420  fmptco  5813  fvtp1g  5862  dff13  5909  fcof1o  5930  isocnv  5952  isores2  5954  isoini  5959  f1oiso2  5968  acexmidlemab  6012  ovmpodf  6153  offval  6243  xp1st  6328  1stconst  6386  cnvf1olem  6389  f1od2  6400  mpoxopoveq  6406  nnaordi  6676  nnmordi  6684  erinxp  6778  dom2lem  6945  fundmen  6981  pw2f1odclem  7020  mapen  7032  ssenen  7037  fidifsnen  7057  difinfsnlem  7298  fodjum  7345  cc2lem  7485  ltsonq  7618  lt2addnq  7624  lt2mulnq  7625  ltexnqq  7628  prarloclemarch2  7639  enq0sym  7652  genprndl  7741  genprndu  7742  prmuloc  7786  distrlem1prl  7802  distrlem1pru  7803  ltsopr  7816  ltexprlemdisj  7826  ltexprlemfl  7829  ltexprlemfu  7831  addcanprlemu  7835  ltaprg  7839  mulcmpblnrlemg  7960  recexgt0sr  7993  mul4  8311  2addsub  8393  muladd  8563  ltleadd  8626  eqord1  8663  eqord2  8664  divmulap3  8857  divcanap7  8901  divadddivap  8907  lemul2a  9039  lemul12b  9041  ltmuldiv2  9055  ltdivmul  9056  ltdivmul2  9058  ledivmul2  9060  lemuldiv2  9062  lt2msq  9066  cju  9141  zextlt  9572  xrlttr  10030  xrre3  10057  ixxdisj  10138  iooshf  10187  icodisj  10227  iccf1o  10239  zssinfcl  10493  seqf1og  10784  expsubap  10850  bcval5  11026  hashfacen  11101  seq3coll  11107  swrdswrdlem  11286  swrdccatin2  11311  sqrt0rlem  11565  lenegsq  11657  zsumdc  11947  fisum0diag2  12010  prodmodclem2  12140  zproddc  12142  ndvdsadd  12494  lcmdvds  12653  oddpwdclemdc  12747  hashdvds  12795  phisum  12815  pcqmul  12878  pcmpt  12918  4sqlemffi  12971  4sqlem11  12976  ennnfonelemex  13037  grpinvid1  13637  grpinvid2  13638  grplcan  13647  grpnpncan0  13681  dfgrp3mlem  13683  dfgrp3m  13684  grplactcnv  13687  0nsg  13803  eqger  13813  resghm  13849  conjghm  13865  znunit  14676  psrgrp  14702  eltg2  14780  ssnei2  14884  restopnb  14908  txdis1cn  15005  txlm  15006  elbl2ps  15119  elbl2  15120  blininf  15151  xmeter  15163  xmetresbl  15167  bdxmet  15228  metrest  15233  dedekindicc  15360  limcimo  15392  dvmptfsum  15452  plycolemc  15485  dvdsppwf1o  15716  fsumdvdsmul  15718  sgmmul  15723  lgsquadlem1  15809  lgsquadlem2  15810  lgsquad2lem2  15814  upgriswlkdc  16214