Theorem jca2 513

Description: Inference conjoining the consequents of two implications. (Contributed by Rodolfo Medina, 12-Oct-2010.)

Hypotheses

Ref	Expression
jca2.1	⊢ (𝜑 → (𝜓 → 𝜒))
jca2.2	⊢ (𝜓 → 𝜃)

Assertion

Ref	Expression
jca2	⊢ (𝜑 → (𝜓 → (𝜒 ∧ 𝜃)))

Proof of Theorem jca2

Step	Hyp	Ref	Expression
1		jca2.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
2		jca2.2	. . 3 ⊢ (𝜓 → 𝜃)
3	2	a1i 11	. 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:  rr19.28v  3592  preddowncl  6224  ssimaex  6835  onfununi  8143  oaordex  8351  domtriord  8859  findcard3  8987  unfilem1  9008  fodomfib  9023  inf0  9309  inf3lem3  9318  tcel  9434  fidomtri2  9683  alephval3  9797  zorn2lem6  10188  fodomb  10213  eqreznegel  12603  iserodd  16464  cshwsiun  16729  txcn  22685  ssfg  22931  fclsnei  23078  eldmgm  26076  fnrelpredd  32961  cvmlift2lem10  33174  relcnveq3  36383  iss2  36406  elrelscnveq3  36536  jca3  36797  prjspreln0  40369  rfovcnvf1od  41501  mnuop3d  41778