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

Theorem adantllr 481
Description: Deduction adding a conjunct to antecedent. (Contributed by NM, 26-Dec-2004.) (Proof shortened by Wolf Lammen, 4-Dec-2012.)
Hypothesis
Ref Expression
adantl2.1 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
Assertion
Ref Expression
adantllr ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)

Proof of Theorem adantllr
StepHypRef Expression
1 simpl 109 . 2 ((𝜑𝜏) → 𝜑)
2 adantl2.1 . 2 (((𝜑𝜓) ∧ 𝜒) → 𝜃)
31, 2sylanl1 402 1 ((((𝜑𝜏) ∧ 𝜓) ∧ 𝜒) → 𝜃)
Colors of variables: wff set class
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:  ad4ant13  513  ad4ant134  1217  r19.29an  2619  diffifi  6893  fimax2gtrilemstep  6899  cnegexlem3  8132  cnegex  8133  lemul12b  8816  climshftlemg  11305  prodeq2  11560  fprodmodd  11644  lcmdvds  12073  pw2dvdslemn  12159  dfgrp3mlem  12962  tgcl  13495  metss  13925  ivthinclemlr  14046  ivthinclemur  14048
  Copyright terms: Public domain W3C validator