Theorem jca2 516

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

Syntax hints:   → wi 4   ∧ wa 398

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 399

This theorem is referenced by:  rr19.28v  3665  preddowncl  6178  ssimaex  6751  onfununi  7981  oaordex  8187  domtriord  8666  findcard3  8764  unfilem1  8785  fodomfib  8801  inf0  9087  inf3lem3  9096  tcel  9190  fidomtri2  9426  alephval3  9539  zorn2lem6  9926  fodomb  9951  eqreznegel  12337  iserodd  16175  cshwsiun  16436  txcn  22237  ssfg  22483  fclsnei  22630  eldmgm  25602  cvmlift2lem10  32563  relcnveq3  35582  iss2  35605  elrelscnveq3  35735  jca3  35996  prjspreln0  39265  rfovcnvf1od  40356  mnuop3d  40613