Theorem jca2 518

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

Syntax hints:   → wi 4   ∧ wa 400

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 210  df-an 401

This theorem is referenced by:  rr19.28v  3582  preddowncl  6154  ssimaex  6738  onfununi  7989  oaordex  8195  domtriord  8685  findcard3  8787  unfilem1  8808  fodomfib  8824  inf0  9110  inf3lem3  9119  tcel  9213  fidomtri2  9449  alephval3  9563  zorn2lem6  9954  fodomb  9979  eqreznegel  12367  iserodd  16220  cshwsiun  16484  txcn  22319  ssfg  22565  fclsnei  22712  eldmgm  25699  fnrelpredd  32583  cvmlift2lem10  32783  relcnveq3  36011  iss2  36034  elrelscnveq3  36164  jca3  36425  prjspreln0  39938  rfovcnvf1od  41071  mnuop3d  41345