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

This theorem is referenced by:  anc2ri  556  pm5.31  827  fnun  6529  fcof  6607  fcoOLD  6609  mapdom2  8884  fisupg  8992  fiint  9021  dffi3  9120  fiinfg  9188  dfac2b  9817  nnadju  9884  cflm  9937  cfslbn  9954  cardmin  10251  fpwwe2lem11  10328  fpwwe2lem12  10329  elfznelfzob  13421  modsumfzodifsn  13592  dvdsdivcl  15953  isprm5  16340  latjlej1  18086  latmlem1  18102  cnrest2  22345  cnpresti  22347  trufil  22969  stdbdxmet  23577  lgsdir  26385  elwwlks2  28232  orthin  29709  mdbr2  30559  dmdbr2  30566  mdsl2i  30585  atcvat4i  30660  mdsymlem3  30668  wzel  33745  ontgval  34547  poimirlem3  35707  poimirlem4  35708  poimirlem29  35733  poimir  35737  cmtbr4N  37196  cvrat4  37384  cdlemblem  37734  negexpidd  40420  3cubeslem1  40422  ensucne0OLD  41035  itschlc0xyqsol  46001  elpglem2  46303