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  6632  fcof  6711  brinxper  8700  mapdom2  9112  fisupg  9235  fiint  9277  fiintOLD  9278  dffi3  9382  fiinfg  9452  dfac2b  10084  nnadju  10151  cflm  10203  cfslbn  10220  cardmin  10517  fpwwe2lem11  10594  fpwwe2lem12  10595  elfznelfzob  13734  modsumfzodifsn  13909  dvdsdivcl  16286  isprm5  16677  latjlej1  18412  latmlem1  18428  cnrest2  23173  cnpresti  23175  trufil  23797  stdbdxmet  24403  lgsdir  27243  elwwlks2  29896  orthin  31375  mdbr2  32225  dmdbr2  32232  mdsl2i  32251  atcvat4i  32326  mdsymlem3  32334  wzel  35812  ontgval  36419  poimirlem3  37617  poimirlem4  37618  poimirlem29  37643  poimir  37647  cmtbr4N  39248  cvrat4  39437  cdlemblem  39787  negexpidd  42670  3cubeslem1  42672  tfsconcatb0  43333  ensucne0OLD  43519  itschlc0xyqsol  48756  elpglem2  49701