Theorem jctild 527

Description: Deduction conjoining a theorem to left of consequent in an implication. (Contributed by NM, 21-Apr-2005.)

Hypotheses

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

Assertion

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

Proof of Theorem jctild

Step	Hyp	Ref	Expression
1		jctild.2	. . 3 ⊢ (𝜑 → 𝜃)
2	1	a1d 25	. 2 ⊢ (𝜑 → (𝜓 → 𝜃))
3		jctild.1	. 2 ⊢ (𝜑 → (𝜓 → 𝜒))
4	2, 3	jcad 514	1 ⊢ (𝜑 → (𝜓 → (𝜃 ∧ 𝜒)))

Syntax hints:   → wi 4   ∧ wa 397

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 398

This theorem is referenced by:  anc2li  557  equvini  2453  2reu1  3835  frpoinsg  6261  ordunidif  6329  isofrlem  7243  dfwe2  7656  orduniorsuc  7709  poxp  8000  fnse  8005  ssenen  8976  dffi3  9234  fpwwe2lem12  10444  zmulcl  12415  rpneg  12808  rexuz3  15105  cau3lem  15111  climrlim2  15301  o1rlimmul  15373  iseralt  15441  gcdzeq  16307  isprm3  16433  vdwnnlem2  16742  ablfaclem3  19735  epttop  22204  lmcnp  22500  dfconn2  22615  txcnp  22816  cmphaushmeo  22996  isfild  23054  cnpflf2  23196  flimfnfcls  23224  alexsubALT  23247  fgcfil  24480  bcthlem5  24537  ivthlem2  24661  ivthlem3  24662  dvfsumrlim  25240  plypf1  25418  axeuclidlem  27375  usgr2wlkneq  28169  wwlksnredwwlkn0  28306  wwlksnextwrd  28307  clwlkclwwlklem2a1  28401  lnon0  29205  hstles  30638  mdsl1i  30728  atcveq0  30755  atcvat4i  30804  cdjreui  30839  issgon  32136  connpconn  33242  tfisg  33831  noetalem1  33989  outsideofrflx  34474  isbasisrelowllem1  35570  isbasisrelowllem2  35571  poimirlem3  35824  poimirlem29  35850  poimir  35854  heicant  35856  equivtotbnd  35980  ismtybndlem  36008  cvrat4  37499  linepsubN  37808  pmapsub  37824  osumcllem4N  38015  pexmidlem1N  38026  dochexmidlem1  39516  harval3  41183  clcnvlem  41269  iccpartimp  44927  sbgoldbwt  45287  sbgoldbst  45288  elsetrecslem  46462