Theorem jctird 526

Description: Deduction conjoining a theorem to right of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

Ref	Expression
jctird.1	⊢ (𝜑 → (𝜓 → 𝜒))
jctird.2	⊢ (𝜑 → 𝜃)

Assertion

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

Proof of Theorem jctird

Step	Hyp	Ref	Expression
1		jctird.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jctird.2	. . 3 ⊢ (𝜑 → 𝜃)
3	2	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
4	1, 3	jcad 512	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 395

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This theorem depends on definitions:  df-bi 207  df-an 396

This theorem is referenced by:  anc2ri  556  pm5.31  830  fnun  6596  fcof  6675  brinxper  8654  mapdom2  9065  fisupg  9177  fiint  9216  fiintOLD  9217  dffi3  9321  fiinfg  9391  dfac2b  10025  nnadju  10092  cflm  10144  cfslbn  10161  cardmin  10458  fpwwe2lem11  10535  fpwwe2lem12  10536  elfznelfzob  13676  modsumfzodifsn  13851  dvdsdivcl  16227  isprm5  16618  latjlej1  18359  latmlem1  18375  cnrest2  23171  cnpresti  23173  trufil  23795  stdbdxmet  24401  lgsdir  27241  elwwlks2  29911  orthin  31390  mdbr2  32240  dmdbr2  32247  mdsl2i  32266  atcvat4i  32341  mdsymlem3  32349  tz9.1regs  35067  wzel  35802  ontgval  36409  poimirlem3  37607  poimirlem4  37608  poimirlem29  37633  poimir  37637  cmtbr4N  39238  cvrat4  39426  cdlemblem  39776  negexpidd  42659  3cubeslem1  42661  tfsconcatb0  43321  ensucne0OLD  43507  itschlc0xyqsol  48756  elpglem2  49701