ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  adantrr GIF version

Theorem adantrr 470
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
StepHypRef Expression
1 simpl 108 . 2 ((𝜓𝜃) → 𝜓)
2 adant2.1 . 2 ((𝜑𝜓) → 𝜒)
31, 2sylan2 284 1 ((𝜑 ∧ (𝜓𝜃)) → 𝜒)
Colors of variables: wff set class
Syntax hints:  wi 4  wa 103
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107
This theorem is referenced by:  ad2ant2r  500  ad2ant2lr  501  dn1dc  944  3ad2antr1  1146  xordidc  1377  po2nr  4231  sotricim  4245  fmptco  5586  fvtp1g  5628  dff13  5669  fcof1o  5690  isocnv  5712  isores2  5714  isoini  5719  f1oiso2  5728  acexmidlemab  5768  ovmpodf  5902  offval  5989  xp1st  6063  1stconst  6118  cnvf1olem  6121  f1od2  6132  mpoxopoveq  6137  nnaordi  6404  nnmordi  6412  erinxp  6503  dom2lem  6666  fundmen  6700  mapen  6740  ssenen  6745  fidifsnen  6764  difinfsnlem  6984  fodjum  7018  cc2lem  7088  ltsonq  7220  lt2addnq  7226  lt2mulnq  7227  ltexnqq  7230  prarloclemarch2  7241  enq0sym  7254  genprndl  7343  genprndu  7344  prmuloc  7388  distrlem1prl  7404  distrlem1pru  7405  ltsopr  7418  ltexprlemdisj  7428  ltexprlemfl  7431  ltexprlemfu  7433  addcanprlemu  7437  ltaprg  7441  mulcmpblnrlemg  7562  recexgt0sr  7595  mul4  7908  2addsub  7990  muladd  8160  ltleadd  8222  eqord1  8259  eqord2  8260  divmulap3  8451  divcanap7  8495  divadddivap  8501  lemul2a  8631  lemul12b  8633  ltmuldiv2  8647  ltdivmul  8648  ltdivmul2  8650  ledivmul2  8652  lemuldiv2  8654  lt2msq  8658  cju  8733  zextlt  9157  xrlttr  9595  xrre3  9619  ixxdisj  9700  iooshf  9749  icodisj  9789  iccf1o  9801  expsubap  10355  bcval5  10523  hashfacen  10593  seq3coll  10599  sqrt0rlem  10789  lenegsq  10881  zsumdc  11167  fisum0diag2  11230  prodmodclem2  11360  ndvdsadd  11641  zssinfcl  11654  lcmdvds  11773  oddpwdclemdc  11864  hashdvds  11910  ennnfonelemex  11940  eltg2  12238  ssnei2  12342  restopnb  12366  txdis1cn  12463  txlm  12464  elbl2ps  12577  elbl2  12578  blininf  12609  xmeter  12621  xmetresbl  12625  bdxmet  12686  metrest  12691  dedekindicc  12796  limcimo  12819
  Copyright terms: Public domain W3C validator