MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  imim12d Structured version   Visualization version   GIF version

Theorem imim12d 81
Description: Deduction combining antecedents and consequents. Deduction associated with imim12 105 and imim12i 62. (Contributed by NM, 7-Aug-1994.) (Proof shortened by Mel L. O'Cat, 30-Oct-2011.)
Hypotheses
Ref Expression
imim12d.1 (𝜑 → (𝜓𝜒))
imim12d.2 (𝜑 → (𝜃𝜏))
Assertion
Ref Expression
imim12d (𝜑 → ((𝜒𝜃) → (𝜓𝜏)))

Proof of Theorem imim12d
StepHypRef Expression
1 imim12d.1 . 2 (𝜑 → (𝜓𝜒))
2 imim12d.2 . . 3 (𝜑 → (𝜃𝜏))
32imim2d 57 . 2 (𝜑 → ((𝜒𝜃) → (𝜒𝜏)))
41, 3syl5d 73 1 (𝜑 → ((𝜒𝜃) → (𝜓𝜏)))
Colors of variables: wff setvar class
Syntax hints:  wi 4
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7
This theorem is referenced by:  imim1d  82  orim12dALT  936  nfimd  1993  rspcimdv  3497  peano5  7322  isf34lem6  9489  inar1  9884  supsrlem  10219  r19.29uz  14428  o1of2  14681  o1rlimmul  14687  caucvg  14747  isprm5  15749  mrissmrid  16613  kgen2ss  21684  txlm  21777  isr0  21866  metcnpi3  22676  addcnlem  22992  nmhmcn  23244  aalioulem5  24429  xrlimcnp  25044  dmdmd  29677  mdsl0  29687  mdsl1i  29698  lmxrge0  30507  bnj517  31465  ax8dfeq  32209  bj-mo3OLD  33320  bj-ax9-2  33375  poimirlem29  33920  heicant  33926  ispridlc  34349  intabssd  38688  ss2iundf  38723
  Copyright terms: Public domain W3C validator