Theorem jctird 528

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 514	1 ⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Syntax hints:   → wi 4   ∧ wa 397

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 206  df-an 398

This theorem is referenced by:  anc2ri  558  pm5.31  830  fnun  6664  fcof  6741  fcoOLD  6743  mapdom2  9148  fisupg  9291  fiint  9324  dffi3  9426  fiinfg  9494  dfac2b  10125  nnadju  10192  cflm  10245  cfslbn  10262  cardmin  10559  fpwwe2lem11  10636  fpwwe2lem12  10637  elfznelfzob  13738  modsumfzodifsn  13909  dvdsdivcl  16259  isprm5  16644  latjlej1  18406  latmlem1  18422  cnrest2  22790  cnpresti  22792  trufil  23414  stdbdxmet  24024  lgsdir  26835  elwwlks2  29251  orthin  30730  mdbr2  31580  dmdbr2  31587  mdsl2i  31606  atcvat4i  31681  mdsymlem3  31689  wzel  34827  ontgval  35364  poimirlem3  36539  poimirlem4  36540  poimirlem29  36565  poimir  36569  cmtbr4N  38173  cvrat4  38362  cdlemblem  38712  negexpidd  41468  3cubeslem1  41470  tfsconcatb0  42142  ensucne0OLD  42329  itschlc0xyqsol  47501  elpglem2  47805