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  3661  preddowncl  6174  ssimaex  6747  onfununi  7977  oaordex  8183  domtriord  8662  findcard3  8760  unfilem1  8781  fodomfib  8797  inf0  9083  inf3lem3  9092  tcel  9186  fidomtri2  9422  alephval3  9535  zorn2lem6  9922  fodomb  9947  eqreznegel  12333  iserodd  16171  cshwsiun  16432  txcn  22233  ssfg  22479  fclsnei  22626  eldmgm  25598  cvmlift2lem10  32559  relcnveq3  35577  iss2  35600  elrelscnveq3  35730  jca3  35991  prjspreln0  39257  rfovcnvf1od  40348  mnuop3d  40605