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  6614  fcof  6693  brinxper  8677  mapdom2  9089  fisupg  9211  fiint  9253  fiintOLD  9254  dffi3  9358  fiinfg  9428  dfac2b  10060  nnadju  10127  cflm  10179  cfslbn  10196  cardmin  10493  fpwwe2lem11  10570  fpwwe2lem12  10571  elfznelfzob  13710  modsumfzodifsn  13885  dvdsdivcl  16262  isprm5  16653  latjlej1  18394  latmlem1  18410  cnrest2  23206  cnpresti  23208  trufil  23830  stdbdxmet  24436  lgsdir  27276  elwwlks2  29946  orthin  31425  mdbr2  32275  dmdbr2  32282  mdsl2i  32301  atcvat4i  32376  mdsymlem3  32384  wzel  35805  ontgval  36412  poimirlem3  37610  poimirlem4  37611  poimirlem29  37636  poimir  37640  cmtbr4N  39241  cvrat4  39430  cdlemblem  39780  negexpidd  42663  3cubeslem1  42665  tfsconcatb0  43326  ensucne0OLD  43512  itschlc0xyqsol  48749  elpglem2  49694