Theorem jctird 534

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

Syntax hints:   → wi 4   ∧ wa 399

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 209  df-an 400

This theorem is referenced by:  anc2ri  564  pm5.31  841  fnun  6635  fcof  6715  brinxper  8708  mapdom2  9120  fisupg  9232  fiint  9271  dffi3  9377  fiinfg  9447  dfac2b  10087  nnadju  10154  cflm  10206  cfslbn  10224  cardmin  10521  fpwwe2lem11  10599  fpwwe2lem12  10600  elfznelfzob  13780  modsumfzodifsn  13957  dvdsdivcl  16350  isprm5  16742  latjlej1  18485  latmlem1  18501  chnccat  18658  cnrest2  23346  cnpresti  23348  trufil  23970  stdbdxmet  24575  lgsdir  27396  elwwlks2  30169  orthin  31649  mdbr2  32499  dmdbr2  32506  mdsl2i  32525  atcvat4i  32600  mdsymlem3  32608  tz9.1regs  35430  wzel  36172  ontgval  36791  poimirlem3  38122  poimirlem4  38123  poimirlem29  38148  poimir  38152  suceldisj  39317  cmtbr4N  39879  cvrat4  40067  cdlemblem  40417  negexpidd  43263  3cubeslem1  43265  tfsconcatb0  43921  ensucne0OLD  44106  itschlc0xyqsol  49389  elpglem2  50333